-lemma cnr_lift: ∀L0,L,T,T0,d,e.
- â¦\83G, Lâ¦\84 â\8a¢ ð\9d\90\8dâ¦\83Tâ¦\84 â\86\92 â\87©[d, e] L0 â\89¡ L â\86\92 â\87§[d, e] T â\89¡ T0 â\86\92 L0 ⊢ 𝐍⦃T0⦄.
-#L0 #L #T #T0 #d #e #HLT #HL0 #HT0 #X #H
+lemma cnr_lift: ∀G,L0,L,T,T0,d,e. ⦃G, L⦄ ⊢ 𝐍⦃T⦄ →
+ â\87©[d, e] L0 â\89¡ L â\86\92 â\87§[d, e] T â\89¡ T0 â\86\92 â¦\83G, L0â¦\84 ⊢ 𝐍⦃T0⦄.
+#G #L0 #L #T #T0 #d #e #HLT #HL0 #HT0 #X #H