-lemma csx_fwd_applv: ∀h,o,G,L,T,Vs. ⦃G, L⦄ ⊢ ⬊*[h, o] Ⓐ Vs.T →
- â¦\83G, Lâ¦\84 â\8a¢ â¬\8a*[h, o] Vs â\88§ â¦\83G, Lâ¦\84 â\8a¢ â¬\8a*[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❫ →
+ â\9dªG,Lâ\9d« â\8a¢ â¬\88*[h] ð\9d\90\92â\9dªVsâ\9d« â\88§ â\9dªG,Lâ\9d« â\8a¢ â¬\88*[h] ð\9d\90\92â\9dªTâ\9d«.
+#h #G #L #T #Vs elim Vs -Vs /2 width=1 by conj/