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