-lemma csx_applv_cnx: ∀h,G,L,T. 𝐒⦃T⦄ → ⦃G,L⦄ ⊢ ⬈[h] 𝐍⦃T⦄ →
- ∀Vs. ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃Vs⦄ → ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃ⒶVs.T⦄.
-#h #G #L #T #H1T #H2T #Vs elim Vs -Vs
-[ #_ normalize in ⊢ (????%); /2 width=1 by cnx_csx/
+lemma csx_applv_cnx (G) (L):
+ ∀T. 𝐒❪T❫ → ❪G,L❫ ⊢ ⬈𝐍 T →
+ ∀Vs. ❪G,L❫ ⊢ ⬈*𝐒 Vs → ❪G,L❫ ⊢ ⬈*𝐒 ⒶVs.T.
+#G #L #T #H1T #H2T #Vs elim Vs -Vs
+[ #_ normalize in ⊢ (???%); /2 width=1 by cnx_csx/