-lemma cpxs_fwd_beta (h) (p) (G) (L):
- ∀V,W,T,X2. ❪G,L❫ ⊢ ⓐV.ⓛ[p]W.T ⬈*[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):
+ ∀V,W,T,X2. ❪G,L❫ ⊢ ⓐV.ⓛ[p]W.T ⬈* 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 *