-fact csx_appl_theta_aux: ∀h,p,G,L,U. ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃U⦄ → ∀V1,V2. ⬆*[1] V1 ≘ V2 →
- ∀V,T. U = ⓓ{p}V.ⓐV2.T → ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃ⓐV1.ⓓ{p}V.T⦄.
-#h #p #G #L #X #H
+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
+/2 width=1 by csx_abbr, csx_abst/
+qed.
+
+fact csx_appl_theta_aux (G) (L):
+ ∀p,U. ❨G,L❩ ⊢ ⬈*𝐒 U → ∀V1,V2. ⇧[1] V1 ≘ V2 →
+ ∀V,T. U = ⓓ[p]V.ⓐV2.T → ❨G,L❩ ⊢ ⬈*𝐒 ⓐV1.ⓓ[p]V.T.
+#G #L #p #X #H