-lemma csx_bind (h) (G):
- ∀p,I,L,V. ❪G,L❫ ⊢ ⬈*[h] 𝐒❪V❫ →
- ∀T. ❪G,L.ⓑ[I]V❫ ⊢ ⬈*[h] 𝐒❪T❫ → ❪G,L❫ ⊢ ⬈*[h] 𝐒❪ⓑ[p,I]V.T❫.
-#h #G #p * #L #V #HV #T #HT
+lemma csx_bind (h) (G) (L):
+ ∀p,I,V. ❪G,L❫ ⊢ ⬈*𝐒[h] V →
+ ∀T. ❪G,L.ⓑ[I]V❫ ⊢ ⬈*𝐒[h] T → ❪G,L❫ ⊢ ⬈*𝐒[h] ⓑ[p,I]V.T.
+#h #G #L #p * #V #HV #T #HT