-lemma csx_fwd_applv: â\88\80h,o,G,L,T,Vs. â¦\83G, Lâ¦\84 â\8a¢ â¬\8a*[h, o] â\92¶ Vs.T →
- â¦\83G, Lâ¦\84 â\8a¢ â¬\8a*[h, o] Vs â\88§ â¦\83G, Lâ¦\84 â\8a¢ â¬\8a*[h, o] T.
+lemma csx_fwd_applv: â\88\80h,o,G,L,T,Vs. â¦\83G, Lâ¦\84 â\8a¢ â¬\88*[h, o] ð\9d\90\92â¦\83â\92¶Vs.Tâ¦\84 →
+ â¦\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.