blob: b161d95bbf2eed00ecd3b601222c0352ed546a63 [file] [edit]
mutual
inductive Lift : Bool -> Type -> Type 2
inductive Env : List Bool -> Type 2
| cons : Lift t y -> Env [t]
end