-fact csx_appl_beta_aux (h) (G) (L):
- ∀p,U1. ❪G,L❫ ⊢ ⬈*𝐒[h] U1 →
- ∀V,W,T1. U1 = ⓓ[p]ⓝW.V.T1 → ❪G,L❫ ⊢ ⬈*𝐒[h] ⓐV.ⓛ[p]W.T1.
-#h #G #L #p #X #H @(csx_ind … H) -X
+fact csx_appl_beta_aux (G) (L):
+ ∀p,U1. ❪G,L❫ ⊢ ⬈*𝐒 U1 →
+ ∀V,W,T1. U1 = ⓓ[p]ⓝW.V.T1 → ❪G,L❫ ⊢ ⬈*𝐒 ⓐV.ⓛ[p]W.T1.
+#G #L #p #X #H @(csx_ind … H) -X