-lemma cpxs_sort: ∀h,G,L,s,n. ⦃G, L⦄ ⊢ ⋆s ⬈*[h] ⋆((next h)^n s).
-#h #G #L #s #n elim n -n /2 width=1 by cpx_cpxs/
-#n >iter_S /2 width=3 by cpxs_strap1/
-qed.
-
-lemma cpxs_bind_dx: ∀h,G,L,V1,V2. ⦃G, L⦄ ⊢ V1 ⬈[h] V2 →
- ∀I,T1,T2. ⦃G, L. ⓑ{I}V1⦄ ⊢ T1 ⬈*[h] T2 →
- ∀p. ⦃G, L⦄ ⊢ ⓑ{p,I}V1.T1 ⬈*[h] ⓑ{p,I}V2.T2.
-#h #G #L #V1 #V2 #HV12 #I #T1 #T2 #HT12 #a @(cpxs_ind_dx … HT12) -T1
+lemma cpxs_qu (G) (L):
+ ∀s1,s2. ❪G,L❫ ⊢ ⋆s1 ⬈* ⋆s2.
+/2 width=1 by cpx_cpxs/ qed.
+
+lemma cpxs_bind_dx (G) (L):
+ ∀V1,V2. ❪G,L❫ ⊢ V1 ⬈ V2 →
+ ∀I,T1,T2. ❪G,L. ⓑ[I]V1❫ ⊢ T1 ⬈* T2 →
+ ∀p. ❪G,L❫ ⊢ ⓑ[p,I]V1.T1 ⬈* ⓑ[p,I]V2.T2.
+#G #L #V1 #V2 #HV12 #I #T1 #T2 #HT12 #a @(cpxs_ind_dx … HT12) -T1