+| #J #W1 #W2 #T1 #T2 #d #e #HW #HT #I #V2 #U2 #H destruct /2 width=5/
+]
+qed.
+
+(* Basic_1: was: lift_gen_flat *)
+lemma lift_inv_flat2: ∀d,e,T1,I,V2,U2. ⇧[d,e] T1 ≡ ⓕ{I} V2. U2 →
+ ∃∃V1,U1. ⇧[d,e] V1 ≡ V2 & ⇧[d,e] U1 ≡ U2 &
+ T1 = ⓕ{I} V1. U1.
+/2 width=3/ qed-.
+
+lemma lift_inv_pair_xy_x: ∀d,e,I,V,T. ⇧[d, e] ②{I} V. T ≡ V → False.
+#d #e #J #V elim V -V
+[ * #i #T #H
+ [ lapply (lift_inv_sort2 … H) -H #H destruct
+ | elim (lift_inv_lref2 … H) -H * #_ #H destruct
+ | lapply (lift_inv_gref2 … H) -H #H destruct
+ ]
+| * #I #W2 #U2 #IHW2 #_ #T #H
+ [ elim (lift_inv_bind2 … H) -H #W1 #U1 #HW12 #_ #H destruct /2 width=2/
+ | elim (lift_inv_flat2 … H) -H #W1 #U1 #HW12 #_ #H destruct /2 width=2/
+ ]
+]
+qed-.
+
+lemma lift_inv_pair_xy_y: ∀I,T,V,d,e. ⇧[d, e] ②{I} V. T ≡ T → False.
+#J #T elim T -T
+[ * #i #V #d #e #H
+ [ lapply (lift_inv_sort2 … H) -H #H destruct
+ | elim (lift_inv_lref2 … H) -H * #_ #H destruct
+ | lapply (lift_inv_gref2 … H) -H #H destruct
+ ]
+| * #I #W2 #U2 #_ #IHU2 #V #d #e #H
+ [ elim (lift_inv_bind2 … H) -H #W1 #U1 #_ #HU12 #H destruct /2 width=4/
+ | elim (lift_inv_flat2 … H) -H #W1 #U1 #_ #HU12 #H destruct /2 width=4/
+ ]
+]
+qed-.
+
+(* Basic forward lemmas *****************************************************)
+
+lemma tw_lift: ∀d,e,T1,T2. ⇧[d, e] T1 ≡ T2 → #[T1] = #[T2].
+#d #e #T1 #T2 #H elim H -d -e -T1 -T2 normalize //
+qed-.
+
+lemma lift_simple_dx: ∀d,e,T1,T2. ⇧[d, e] T1 ≡ T2 → 𝐒[T1] → 𝐒[T2].
+#d #e #T1 #T2 #H elim H -d -e -T1 -T2 //
+#I #V1 #V2 #T1 #T2 #d #e #_ #_ #_ #_ #H
+elim (simple_inv_bind … H)
+qed-.
+
+lemma lift_simple_sn: ∀d,e,T1,T2. ⇧[d, e] T1 ≡ T2 → 𝐒[T2] → 𝐒[T1].
+#d #e #T1 #T2 #H elim H -d -e -T1 -T2 //
+#I #V1 #V2 #T1 #T2 #d #e #_ #_ #_ #_ #H
+elim (simple_inv_bind … H)
+qed-.
+
+(* Basic properties *********************************************************)
+
+(* Basic_1: was: lift_lref_gt *)
+lemma lift_lref_ge_minus: ∀d,e,i. d + e ≤ i → ⇧[d, e] #(i - e) ≡ #i.
+#d #e #i #H >(plus_minus_m_m i e) in ⊢ (? ? ? ? %); /2 width=2/ /3 width=2/
+qed.
+
+lemma lift_lref_ge_minus_eq: ∀d,e,i,j. d + e ≤ i → j = i - e → ⇧[d, e] #j ≡ #i.
+/2 width=1/ qed-.
+
+(* Basic_1: was: lift_r *)
+lemma lift_refl: ∀T,d. ⇧[d, 0] T ≡ T.
+#T elim T -T
+[ * #i // #d elim (lt_or_ge i d) /2 width=1/
+| * /2 width=1/
+]
+qed.
+
+lemma lift_total: ∀T1,d,e. ∃T2. ⇧[d,e] T1 ≡ T2.
+#T1 elim T1 -T1
+[ * #i /2 width=2/ #d #e elim (lt_or_ge i d) /3 width=2/
+| * #I #V1 #T1 #IHV1 #IHT1 #d #e
+ elim (IHV1 d e) -IHV1 #V2 #HV12
+ [ elim (IHT1 (d+1) e) -IHT1 /3 width=2/
+ | elim (IHT1 d e) -IHT1 /3 width=2/
+ ]
+]
+qed.
+
+(* Basic_1: was: lift_free (right to left) *)
+lemma lift_split: ∀d1,e2,T1,T2. ⇧[d1, e2] T1 ≡ T2 →
+ ∀d2,e1. d1 ≤ d2 → d2 ≤ d1 + e1 → e1 ≤ e2 →
+ ∃∃T. ⇧[d1, e1] T1 ≡ T & ⇧[d2, e2 - e1] T ≡ T2.
+#d1 #e2 #T1 #T2 #H elim H -d1 -e2 -T1 -T2
+[ /3 width=3/
+| #i #d1 #e2 #Hid1 #d2 #e1 #Hd12 #_ #_
+ lapply (lt_to_le_to_lt … Hid1 Hd12) -Hd12 #Hid2 /4 width=3/
+| #i #d1 #e2 #Hid1 #d2 #e1 #_ #Hd21 #He12
+ lapply (transitive_le … (i+e1) Hd21 ?) /2 width=1/ -Hd21 #Hd21
+ >(plus_minus_m_m e2 e1 ?) // /3 width=3/
+| /3 width=3/
+| #I #V1 #V2 #T1 #T2 #d1 #e2 #_ #_ #IHV #IHT #d2 #e1 #Hd12 #Hd21 #He12
+ elim (IHV … Hd12 Hd21 He12) -IHV #V0 #HV0a #HV0b
+ elim (IHT (d2+1) … ? ? He12) /2 width=1/ /3 width=5/
+| #I #V1 #V2 #T1 #T2 #d1 #e2 #_ #_ #IHV #IHT #d2 #e1 #Hd12 #Hd21 #He12
+ elim (IHV … Hd12 Hd21 He12) -IHV #V0 #HV0a #HV0b
+ elim (IHT d2 … ? ? He12) // /3 width=5/