DEFINITION lift_gen_lift()
TYPE =
∀t1:T
.∀x:T
.∀h1:nat
.∀h2:nat
.∀d1:nat
.∀d2:nat
.le d1 d2
→(eq T (lift h1 d1 t1) (lift h2 (plus d2 h1) x)
→ex2 T λt2:T.eq T x (lift h1 d1 t2) λt2:T.eq T t1 (lift h2 d2 t2))
BODY =
Show proof