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