-lemma cpxs_bind_dx (h) (G): ∀L,V1,V2. ⦃G, L⦄ ⊢ V1 ⬈*[h] V2 →
- ∀I,T1,T2. ⦃G, L.ⓑ{I}V2⦄ ⊢ T1 ⬈*[h] T2 →
- ∀p. ⦃G, L⦄ ⊢ ⓑ{p,I}V1.T1 ⬈*[h] ⓑ{p,I}V2.T2.
+lemma cpxs_bind_dx (h) (G): ∀L,V1,V2. ⦃G,L⦄ ⊢ V1 ⬈*[h] V2 →
+ ∀I,T1,T2. ⦃G,L.ⓑ{I}V2⦄ ⊢ T1 ⬈*[h] T2 →
+ ∀p. ⦃G,L⦄ ⊢ ⓑ{p,I}V1.T1 ⬈*[h] ⓑ{p,I}V2.T2.