-fact csx_fwd_bind_dx_aux: ∀h,o,G,L,U. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃U⦄ →
- ∀p,I,V,T. U = ⓑ{p,I}V.T → ⦃G, L.ⓑ{I}V⦄ ⊢ ⬈*[h, o] 𝐒⦃T⦄.
-#h #o #G #L #U #H elim H -H #U0 #_ #IH #p #I #V #T #H destruct
+fact csx_fwd_bind_dx_aux: ∀h,G,L,U. ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃U⦄ →
+ ∀p,I,V,T. U = ⓑ{p,I}V.T → ⦃G,L.ⓑ{I}V⦄ ⊢ ⬈*[h] 𝐒⦃T⦄.
+#h #G #L #U #H elim H -H #U0 #_ #IH #p #I #V #T #H destruct