-lemma csx_fwd_applv: ∀h,o,G,L,T,Vs. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃ⒶVs.T⦄ →
- ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃Vs⦄ ∧ ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T⦄.
-#h #o #G #L #T #Vs elim Vs -Vs /2 width=1 by conj/
+lemma csx_fwd_applv: ∀h,G,L,T,Vs. ⦃G, L⦄ ⊢ ⬈*[h] 𝐒⦃ⒶVs.T⦄ →
+ ⦃G, L⦄ ⊢ ⬈*[h] 𝐒⦃Vs⦄ ∧ ⦃G, L⦄ ⊢ ⬈*[h] 𝐒⦃T⦄.
+#h #G #L #T #Vs elim Vs -Vs /2 width=1 by conj/