-lemma csx_bind (h) (G):
- ∀p,I,L,V. ❪G,L❫ ⊢ ⬈*[h] 𝐒❪V❫ →
- â\88\80T. â\9dªG,L.â\93\91[I]Vâ\9d« â\8a¢ â¬\88*[h] ð\9d\90\92â\9dªTâ\9d« â\86\92 â\9dªG,Lâ\9d« â\8a¢ â¬\88*[h] ð\9d\90\92â\9dªâ\93\91[p,I]V.Tâ\9d«.
-#h #G #p * #L #V #HV #T #HT
+lemma csx_bind (G) (L):
+ ∀p,I,V. ❨G,L❩ ⊢ ⬈*𝐒 V →
+ â\88\80T. â\9d¨G,L.â\93\91[I]Vâ\9d© â\8a¢ â¬\88*ð\9d\90\92 T â\86\92 â\9d¨G,Lâ\9d© â\8a¢ â¬\88*ð\9d\90\92 â\93\91[p,I]V.T.
+#G #L #p * #V #HV #T #HT