-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
+lemma csx_bind (G) (L):
+ ∀p,I,V. ❪G,L❫ ⊢ ⬈*𝐒 V →
+ ∀T. ❪G,L.ⓑ[I]V❫ ⊢ ⬈*𝐒 T → ❪G,L❫ ⊢ ⬈*𝐒 ⓑ[p,I]V.T.
+#G #L #p * #V #HV #T #HT