-fact lifts_inv_cons_aux: ∀T1,T2,des. ⬆*[des] T1 ≡ T2 →
- ∀d,e,tl. des = {d, e} @ tl →
- ∃∃T. ⬆[d, e] T1 ≡ T & ⬆*[tl] T ≡ T2.
-#T1 #T2 #des * -T1 -T2 -des
-[ #T #d #e #tl #H destruct
-| #T1 #T #T2 #des #d #e #HT1 #HT2 #hd #he #tl #H destruct
+fact lifts_inv_cons_aux: ∀T1,T2,cs. ⬆*[cs] T1 ≡ T2 →
+ ∀l,m,tl. cs = {l, m} @ tl →
+ ∃∃T. ⬆[l, m] T1 ≡ T & ⬆*[tl] T ≡ T2.
+#T1 #T2 #cs * -T1 -T2 -cs
+[ #T #l #m #tl #H destruct
+| #T1 #T #T2 #cs #l #m #HT1 #HT2 #l0 #m0 #tl #H destruct