-lemma cnx_inv_appl: ∀h,o,G,L,V,T. ⦃G, L⦄ ⊢ ⬈[h, o] 𝐍⦃ⓐV.T⦄ →
- â\88§â\88§ â¦\83G, Lâ¦\84 â\8a¢ â¬\88[h, o] ð\9d\90\8dâ¦\83Vâ¦\84 & â¦\83G, Lâ¦\84 â\8a¢ â¬\88[h, o] ð\9d\90\8dâ¦\83Tâ¦\84 & ð\9d\90\92â¦\83Tâ¦\84.
-#h #o #G #L #V1 #T1 #HVT1 @and3_intro
+lemma cnx_inv_appl: ∀h,G,L,V,T. ❪G,L❫ ⊢ ⬈[h] 𝐍❪ⓐV.T❫ →
+ â\88§â\88§ â\9dªG,Lâ\9d« â\8a¢ â¬\88[h] ð\9d\90\8dâ\9dªVâ\9d« & â\9dªG,Lâ\9d« â\8a¢ â¬\88[h] ð\9d\90\8dâ\9dªTâ\9d« & ð\9d\90\92â\9dªTâ\9d«.
+#h #G #L #V1 #T1 #HVT1 @and3_intro