-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 (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