]
qed.
+lemma lift_total: ∀T1,d,e. ∃T2. ↑[d,e] T1 ≡ T2.
+#T1 elim T1 -T1
+[ /2/
+| #i #d #e elim (lt_or_ge i d) /3/
+| * #I #V1 #T1 #IHV1 #IHT1 #d #e
+ elim (IHV1 d e) -IHV1 #V2 #HV12
+ [ elim (IHT1 (d+1) e) -IHT1 /3/
+ | elim (IHT1 d e) -IHT1 /3/
+ ]
+]
+qed.
+
(* Basic inversion lemmas ***************************************************)
lemma lift_inv_refl_aux: ∀d,e,T1,T2. ↑[d, e] T1 ≡ T2 → e = 0 → T1 = T2.