-lemma cpxs_sort: ∀h,g,G,L,k,l1. deg h g k l1 →
- ∀l2. l2 ≤ l1 → ⦃G, L⦄ ⊢ ⋆k ➡*[h, g] ⋆((next h)^l2 k).
-#h #g #G #L #k #l1 #Hkl1 #l2 @(nat_ind_plus … l2) -l2 /2 width=1 by cpx_cpxs/
-#l2 #IHl2 #Hl21 >iter_SO
-@(cpxs_strap1 … (⋆(iter l2 ℕ (next h) k)))
+lemma cpxs_sort: ∀h,g,G,L,k,d1. deg h g k d1 →
+ ∀d2. d2 ≤ d1 → ⦃G, L⦄ ⊢ ⋆k ➡*[h, g] ⋆((next h)^d2 k).
+#h #g #G #L #k #d1 #Hkd1 #d2 @(nat_ind_plus … d2) -d2 /2 width=1 by cpx_cpxs/
+#d2 #IHd2 #Hd21 >iter_SO
+@(cpxs_strap1 … (⋆(iter d2 ℕ (next h) k)))