-lemma sstas_total_S: ∀h,g,L,l,T,U. ⦃h, L⦄ ⊢ T•[g, l + 1]U →
- ∃∃W. ⦃h, L⦄ ⊢ T •*[g] W & ⦃h, L⦄ ⊢ U •*[g] W.
-#h #g #L #l @(nat_ind_plus … l) -l
-[ #T #U #HTU
- elim (ssta_fwd_correct … HTU) /4 width=4/
-| #l #IHl #T #U #HTU
- elim (ssta_fwd_correct … HTU) <minus_plus_m_m #V #HUV
- elim (IHl … HUV) -IHl -HUV /3 width=4/
-]
+lemma sstas_fwd_correct: ∀h,g,G,L,T1,U1,l1. ⦃G, L⦄ ⊢ T1 •[h, g] ⦃l1, U1⦄ →
+ ∀T2. ⦃G, L⦄ ⊢ T1 •*[h, g] T2 →
+ ∃∃U2,l2. ⦃G, L⦄ ⊢ T2 •[h, g] ⦃l2, U2⦄.
+#h #g #G #L #T1 #U1 #l1 #HTU1 #T2 #H @(sstas_ind … H) -T2 [ /2 width=3/ ] -HTU1
+#T #T2 #l #_ #HT2 * #U #l0 #_ -l0
+elim (ssta_fwd_correct … HT2) -T /2 width=3/