include "Term/defs.ma".
-inductive Lift: Bool \to Nat \to Nat \to Term \to Term \to Prop \def
- | lift_sort : \forall l,q,i,h.
- Lift q l i (leaf (sort h)) (leaf (sort h))
- | lift_lref : \forall l,i,j.
- Lift false l i (leaf (lref j)) (leaf (lref j))
- | lift_lref_lt: \forall l,i,j. j < i \to
- Lift true l i (leaf (lref j)) (leaf (lref j))
- | lift_lref_ge: \forall l,i,j1. i <= j1 \to
- \forall j2. (j1 + l == j2) \to
- Lift true l i (leaf (lref j1)) (leaf (lref j2))
- | lift_bind : \forall l,i,u1,u2. Lift true l i u1 u2 \to
- \forall q,t1,t2. Lift q l (succ i) t1 t2 \to
- \forall r.
- Lift q l i (head q (bind r) u1 t1) (head q (bind r) u2 t2)
- | lift_flat : \forall l,i,u1,u2. Lift true l i u1 u2 \to
- \forall q,t1,t2. Lift q l i t1 t2 \to
- \forall r.
- Lift q l i (head q (flat r) u1 t1) (head q (flat r) u2 t2)
- | lift_head : \forall l,q,p. (p = q \to False) \to
- \forall i,u1,u2. Lift false l i u1 u2 \to
- \forall t1,t2. Lift q l i t1 t2 \to
- \forall z.
- Lift q l i (head p z u1 t1) (head p z u2 t2)
+inductive Lift (l: Nat): Nat \to Term \to Term \to Prop \def
+ | lift_sort : \forall i,h.
+ Lift l i (leaf (sort h)) (leaf (sort h))
+ | lift_lref_gt: \forall i,j. i > j \to
+ Lift l i (leaf (lref j)) (leaf (lref j))
+ | lift_lref_le: \forall i,j1. i <= j1 \to
+ \forall j2. (l + j1 == j2) \to
+ Lift l i (leaf (lref j1)) (leaf (lref j2))
+ | lift_bind : \forall i,u1,u2. Lift l i u1 u2 \to
+ \forall t1,t2. Lift l (succ i) t1 t2 \to
+ \forall r. Lift l i (intb r u1 t1) (intb r u2 t2)
+ | lift_flat : \forall i,u1,u2. Lift l i u1 u2 \to
+ \forall t1,t2. Lift l i t1 t2 \to
+ \forall r. Lift l i (intf r u1 t1) (intf r u2 t2)
.