+qed.
+
+lemma lift_inv_lref2_aux: ∀d,e,T1,T2. ↑[d,e] T1 ≡ T2 → ∀i. T2 = #i →
+ (i < d ∧ T1 = #i) ∨ (d + e ≤ i ∧ T1 = #(i - e)).
+#d #e #T1 #T2 #H elim H -H d e T1 T2
+ [ #k #d #e #i #H destruct
+ | #j #d #e #Hj #i #Hi destruct /3/
+ | #j #d #e #Hj #i #Hi destruct <minus_plus_m_m /4/
+ | #I #V1 #V2 #T1 #T2 #d #e #_ #_ #_ #_ #i #H destruct
+ ]
+qed.
+
+lemma lift_inv_lref2: ∀d,e,T1,i. ↑[d,e] T1 ≡ #i →
+ (i < d ∧ T1 = #i) ∨ (d + e ≤ i ∧ T1 = #(i - e)).
+#d #e #T1 #i #H lapply (lift_inv_lref2_aux … H) /2/
+qed.
+
+lemma lift_inv_con22_aux: ∀d,e,T1,T2. ↑[d,e] T1 ≡ T2 →
+ ∀I,V2,U2. T2 = ♭I V2.U2 →
+ ∃V1,U1. ↑[d,e] V1 ≡ V2 ∧ ↑[d+1,e] U1 ≡ U2 ∧
+ T1 = ♭I V1.U1.
+#d #e #T1 #T2 #H elim H -H d e T1 T2
+ [ #k #d #e #I #V2 #U2 #H destruct
+ | #i #d #e #_ #I #V2 #U2 #H destruct
+ | #i #d #e #_ #I #V2 #U2 #H destruct
+ | #J #W1 #W2 #T1 #T2 #d #e #HW #HT #_ #_ #I #V2 #U2 #H destruct /5/
+qed.
+
+lemma lift_inv_con22: ∀d,e,T1,I,V2,U2. ↑[d,e] T1 ≡ ♭I V2. U2 →
+ ∃V1,U1. ↑[d,e] V1 ≡ V2 ∧ ↑[d+1,e] U1 ≡ U2 ∧
+ T1 = ♭I V1. U1.
+#d #e #T1 #I #V2 #U2 #H lapply (lift_inv_con22_aux … H) /2/
+qed.
+
+(* the main properies *******************************************************)
+
+axiom lift_trans_rev: ∀d1,e1,T1,T. ↑[d1,e1] T1 ≡ T →
+ ∀d2,e2,T2. ↑[d2 + e1, e2] T2 ≡ T →
+ d1 ≤ d2 →
+ ∃T0. ↑[d1, e1] T0 ≡ T2 ∧ ↑[d2, e2] T0 ≡ T1.