-(* Basic_1: was: lift_r *)
-lemma lift_refl: ∀T,l. ⬆[l, 0] T ≡ T.
-#T elim T -T
-[ * #i // #l elim (lt_or_ge i l) /2 width=1 by lift_lref_lt,
-lift_lref_ge/
-| * /2 width=1 by lift_bind, lift_flat/
-]
-qed.
-
-lemma lift_total: ∀T1,l,m. ∃T2. ⬆[l,m] T1 ≡ T2.
-#T1 elim T1 -T1
-[ * #i /2 width=2 by lift_sort, lift_gref, ex_intro/
- #l #m elim (lt_or_ge i l) /3 width=2 by lift_lref_lt, lift_lref_ge,
-ex_intro/
-| * [ #a ] #I #V1 #T1 #IHV1 #IHT1 #l #m
- elim (IHV1 l m) -IHV1 #V2 #HV12
- [ elim (IHT1 (l+1) m) -IHT1 /3 width=2 by lift_bind, ex_intro/
- | elim (IHT1 l m) -IHT1 /3 width=2 by lift_flat, ex_intro/
- ]
-]
-qed.
-
-lemma liftv_total: ∀l,m. ∀T1s:list term. ∃T2s. ⬆[l, m] T1s ≡ T2s.
-#l #m #T1s elim T1s -T1s
-[ /2 width=2 by liftv_nil, ex_intro/
-| #T1 #T1s * #T2s #HT12s
- elim (lift_total T1 l m) /3 width=2 by liftv_cons, ex_intro/
-]
-qed-.