-lemma csx_applv_beta (h) (G):
- ∀p,L,Vs,V,W,T. ❪G,L❫ ⊢ ⬈*[h] 𝐒❪ⒶVs.ⓓ[p]ⓝW.V.T❫ →
- â\9dªG,Lâ\9d« â\8a¢ â¬\88*[h] ð\9d\90\92â\9dªâ\92¶Vs.â\93\90V.â\93\9b[p]W.Tâ\9d«.
-#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/