-lemma lstas_inv_O: ∀h,G,L,T,U. ⦃G, L⦄ ⊢ T •*[h, 0] U → T = U.
-/2 width=4 by lstar_inv_O/ qed-.
-
-lemma lstas_inv_SO: ∀h,G,L,T,U. ⦃G, L⦄ ⊢ T •*[h, 1] U → ⦃G, L⦄ ⊢ T •[h] U.
-/2 width=1 by lstar_inv_step/ qed-.
-
-lemma lstas_inv_step_sn: ∀h,G,L,T1,T2,l. ⦃G, L⦄ ⊢ T1 •*[h, l+1] T2 →
- ∃∃T. ⦃G, L⦄ ⊢ T1 •[h] T & ⦃G, L⦄ ⊢ T •*[h, l] T2.
-/2 width=3 by lstar_inv_S/ qed-.
-
-lemma lstas_inv_step_dx: ∀h,G,L,T1,T2,l. ⦃G, L⦄ ⊢ T1 •*[h, l+1] T2 →
- ∃∃T. ⦃G, L⦄ ⊢ T1 •*[h, l] T & ⦃G, L⦄ ⊢ T •[h] T2.
-/2 width=3 by lstar_inv_S_dx/ qed-.
-
-lemma lstas_inv_sort1: ∀h,G,L,X,k,l. ⦃G, L⦄ ⊢ ⋆k •*[h, l] X → X = ⋆((next h)^l k).
-#h #G #L #X #k #l #H @(lstas_ind_dx … H) -X -l //
-#l #X #X0 #_ #H #IHX destruct
-lapply (sta_inv_sort1 … H) -H #H destruct
->iter_SO //
+fact lstas_inv_sort1_aux: ∀h,G,L,T,U,d. ⦃G, L⦄ ⊢ T •*[h, d] U → ∀k0. T = ⋆k0 →
+ U = ⋆((next h)^d k0).
+#h #G #L #T #U #d * -G -L -T -U -d
+[ #G #L #d #k #k0 #H destruct //
+| #G #L #K #V #W #U #i #d #_ #_ #_ #k0 #H destruct
+| #G #L #K #W #V #i #_ #_ #k0 #H destruct
+| #G #L #K #W #V #U #i #d #_ #_ #_ #k0 #H destruct
+| #a #I #G #L #V #T #U #d #_ #k0 #H destruct
+| #G #L #V #T #U #d #_ #k0 #H destruct
+| #G #L #W #T #U #d #_ #k0 #H destruct