-lemma csx_applv_beta (h) (G):
- ∀p,L,Vs,V,W,T. ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃ⒶVs.ⓓ{p}ⓝW.V.T⦄ →
- â¦\83G,Lâ¦\84 â\8a¢ â¬\88*[h] ð\9d\90\92â¦\83â\92¶Vs.â\93\90V.â\93\9b{p}W.Tâ¦\84.
-#h #G #p #L #Vs elim Vs -Vs /2 width=1 by csx_appl_beta/
+lemma csx_applv_beta (G) (L):
+ ∀p,Vs,V,W,T. ❪G,L❫ ⊢ ⬈*𝐒 ⒶVs.ⓓ[p]ⓝW.V.T →
+ â\9dªG,Lâ\9d« â\8a¢ â¬\88*ð\9d\90\92 â\92¶Vs.â\93\90V.â\93\9b[p]W.T.
+#G #L #p #Vs elim Vs -Vs /2 width=1 by csx_appl_beta/