inductive Lift: Nat \to Nat \to Proof \to Proof \to Prop \def
| lift_lref_lt: \forall jd,jh,i. i < jd \to Lift jd jh (lref i) (lref i)
inductive Lift: Nat \to Nat \to Proof \to Proof \to Prop \def
| lift_lref_lt: \forall jd,jh,i. i < jd \to Lift jd jh (lref i) (lref i)