-lemma cnx_inv_lift: ∀h,g,L0,L,T,T0,d,e. ⦃h, L0⦄ ⊢ 𝐍[h, g]⦃T0⦄ → ⇩[d, e] L0 ≡ L →
- â\87§[d, e] T â\89¡ T0 â\86\92 â¦\83G, Lâ¦\84 â\8a¢ ð\9d\90\8d[h, g]⦃T⦄.
-#h #g #L0 #L #T #T0 #d #e #HLT0 #HL0 #HT0 #X #H
-elim (lift_total X d e) #X0 #HX0
+lemma cnx_inv_lift: ∀h,g,G,L0,L,T,T0,s,l,m. ⦃G, L0⦄ ⊢ ➡[h, g] 𝐍⦃T0⦄ → ⬇[s, l, m] L0 ≡ L →
+ â¬\86[l, m] T â\89¡ T0 â\86\92 â¦\83G, Lâ¦\84 â\8a¢ â\9e¡[h, g] ð\9d\90\8d⦃T⦄.
+#h #g #G #L0 #L #T #T0 #s #l #m #HLT0 #HL0 #HT0 #X #H
+elim (lift_total X l m) #X0 #HX0