-lemma cpxs_fwd_beta (h) (p) (G) (L):
- â\88\80V,W,T,X2. â¦\83G,Lâ¦\84 â\8a¢ â\93\90V.â\93\9b{p}W.T â¬\88*[h] X2 →
- ∨∨ ⓐV.ⓛ{p}W.T ⩳ X2 | ⦃G,L⦄ ⊢ ⓓ{p}ⓝW.V.T ⬈*[h] X2.
-#h #p #G #L #V #W #T #X2 #H elim (cpxs_inv_appl1 … H) -H *
+lemma cpxs_fwd_beta (p) (G) (L):
+ â\88\80V,W,T,X2. â\9dªG,Lâ\9d« â\8a¢ â\93\90V.â\93\9b[p]W.T â¬\88* X2 →
+ ∨∨ ⓐV.ⓛ[p]W.T ~ X2 | ❪G,L❫ ⊢ ⓓ[p]ⓝW.V.T ⬈* X2.
+#p #G #L #V #W #T #X2 #H elim (cpxs_inv_appl1 … H) -H *