-lemma csx_applv_cnx (h) (G) (L):
- â\88\80T. ð\9d\90\92â¦\83Tâ¦\84 â\86\92 â¦\83G,Lâ¦\84 â\8a¢ â¬\88[h] ð\9d\90\8dâ¦\83Tâ¦\84 →
- â\88\80Vs. â¦\83G,Lâ¦\84 â\8a¢ â¬\88*[h] ð\9d\90\92â¦\83Vsâ¦\84 â\86\92 â¦\83G,Lâ¦\84 â\8a¢ â¬\88*[h] ð\9d\90\92â¦\83â\92¶Vs.Tâ¦\84.
-#h #G #L #T #H1T #H2T #Vs elim Vs -Vs
-[ #_ normalize in ⊢ (????%); /2 width=1 by cnx_csx/
+lemma csx_applv_cnx (G) (L):
+ â\88\80T. ð\9d\90\92â\9dªTâ\9d« â\86\92 â\9dªG,Lâ\9d« â\8a¢ â¬\88ð\9d\90\8d T →
+ â\88\80Vs. â\9dªG,Lâ\9d« â\8a¢ â¬\88*ð\9d\90\92 Vs â\86\92 â\9dªG,Lâ\9d« â\8a¢ â¬\88*ð\9d\90\92 â\92¶Vs.T.
+#G #L #T #H1T #H2T #Vs elim Vs -Vs
+[ #_ normalize in ⊢ (???%); /2 width=1 by cnx_csx/