-lemma csx_fwd_applv: ∀h,o,G,L,T,Vs. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃ⒶVs.T⦄ →
- â¦\83G, Lâ¦\84 â\8a¢ â¬\88*[h, o] ð\9d\90\92â¦\83Vsâ¦\84 â\88§ â¦\83G, Lâ¦\84 â\8a¢ â¬\88*[h, o] ð\9d\90\92â¦\83Tâ¦\84.
-#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/