-lemma cnx_inv_lift: ∀h,g,G,L0,L,T,T0,s,l,m. ⦃G, L0⦄ ⊢ ➡[h, g] 𝐍⦃T0⦄ → ⬇[s, l, m] L0 ≡ L →
- ⬆[l, m] T ≡ T0 → ⦃G, L⦄ ⊢ ➡[h, g] 𝐍⦃T⦄.
-#h #g #G #L0 #L #T #T0 #s #l #m #HLT0 #HL0 #HT0 #X #H
-elim (lift_total X l m) #X0 #HX0
+lemma cnx_inv_lift: ∀h,o,G,L0,L,T,T0,c,l,k. ⦃G, L0⦄ ⊢ ➡[h, o] 𝐍⦃T0⦄ → ⬇[c, l, k] L0 ≡ L →
+ ⬆[l, k] T ≡ T0 → ⦃G, L⦄ ⊢ ➡[h, o] 𝐍⦃T⦄.
+#h #o #G #L0 #L #T #T0 #c #l #k #HLT0 #HL0 #HT0 #X #H
+elim (lift_total X l k) #X0 #HX0