-lemma lifts_lift_trans: ∀des,i,i0. @⦃i, des⦄ ≡ i0 →
- ∀des0. des + 1 ▭ i + 1 ≡ des0 + 1 →
- â\88\80T1,T0. â\87§*[des0] T1 ≡ T0 →
- â\88\80T2. â\87§[O, i0 + 1] T0 ≡ T2 →
- â\88\83â\88\83T. â\87§[0, i + 1] T1 â\89¡ T & â\87§*[des] T ≡ T2.
-#des elim des -des normalize
-[ #i #x #H1 #des0 #H2 #T1 #T0 #HT10 #T2
+lemma lifts_lift_trans: ∀cs,i,i0. @⦃i, cs⦄ ≡ i0 →
+ ∀cs0. cs + 1 ▭ i + 1 ≡ cs0 + 1 →
+ â\88\80T1,T0. â¬\86*[cs0] T1 ≡ T0 →
+ â\88\80T2. â¬\86[O, i0 + 1] T0 ≡ T2 →
+ â\88\83â\88\83T. â¬\86[0, i + 1] T1 â\89¡ T & â¬\86*[cs] T ≡ T2.
+#cs elim cs -cs normalize
+[ #i #x #H1 #cs0 #H2 #T1 #T0 #HT10 #T2