-lemma csx_fwd_bind: ∀h,o,p,I,G,L,V,T. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃ⓑ{p,I}V.T⦄ →
- â¦\83G, Lâ¦\84 â\8a¢ â¬\88*[h, o] ð\9d\90\92â¦\83Vâ¦\84 â\88§ â¦\83G, L.â\93\91{I}Vâ¦\84 â\8a¢ â¬\88*[h, o] ð\9d\90\92â¦\83Tâ¦\84.
+lemma csx_fwd_bind: ∀h,p,I,G,L,V,T. ❪G,L❫ ⊢ ⬈*[h] 𝐒❪ⓑ[p,I]V.T❫ →
+ â\9dªG,Lâ\9d« â\8a¢ â¬\88*[h] ð\9d\90\92â\9dªVâ\9d« â\88§ â\9dªG,L.â\93\91[I]Vâ\9d« â\8a¢ â¬\88*[h] ð\9d\90\92â\9dªTâ\9d«.