-lemma sstas_ind_alt: ∀h,g,L,U2. ∀R:predicate term.
- (∀T. ⦃h, L⦄ ⊢ U2 •[g , 0] T → R U2) →
- (∀T,U1,l. ⦃h, L⦄ ⊢ T •[g, l + 1] U1 →
- ⦃h, L⦄ ⊢ U1 •* [g] U2 → R U1 → R T
- ) →
- ∀T. ⦃h, L⦄ ⊢ T •*[g] U2 → R T.
-/3 width=9 by sstas_ind_alt_aux/ qed-.
-
-(* Basic inversion lemmas ***************************************************)
-
-fact sstas_inv_sort1_aux: ∀h,g,L,T,U. ⦃h, L⦄ ⊢ T •*[g] U → ∀k. T = ⋆k →
- ∀l. deg h g k l → U = ⋆((next h)^l k).
-#h #g #L #T #U #H @(sstas_ind_alt … H) -T
-[ #U0 #HU0 #k #H #l #Hkl destruct
- elim (ssta_inv_sort1 … HU0) -L #HkO #_ -U0
- >(deg_mono … Hkl HkO) -g -l //
-| #T0 #U0 #l0 #HTU0 #_ #IHU0 #k #H #l #Hkl destruct
- elim (ssta_inv_sort1 … HTU0) -L #HkS #H destruct
- lapply (deg_mono … Hkl HkS) -Hkl #H destruct
- >(IHU0 (next h k) ? l0) -IHU0 // /2 width=1/ >iter_SO >iter_n_Sm //
-]
-qed.
+lemma sstas_ind_dx: ∀h,g,G,L,U2. ∀R:predicate term.
+ R U2 → (
+ ∀T,U1,l. ⦃G, L⦄ ⊢ T •[h, g] ⦃l+1, U1⦄ → ⦃G, L⦄ ⊢ U1 •* [h, g] U2 →
+ R U1 → R T
+ ) →
+ ∀T. ⦃G, L⦄ ⊢ T •*[h, g] U2 → R T.
+#h #g #G #L #U2 #R #IH1 #IH2 #T #H @(star_ind_l … T H) -T //
+#T #T0 * /2 width=5/
+qed-.