-lemma sstas_ygt: ∀h,g,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 •*[h, g] T2 → (T1 = T2 → ⊥) →
- ⦃G, L, T1⦄ >[h, g] ⦃G, L, T2⦄.
-#h #g #G #L #T1 #T2 #H @(sstas_ind … H) -T2
-[ #H elim H //
-| #T #T2 #l #_ #HT2 #IHT1 #HT12 -HT12
- elim (term_eq_dec T1 T) #H destruct
- [ -IHT1 /3 width=2/
- | lapply (IHT1 … H) -IHT1 -H #HT1
- @(ygt_strap1 … HT1) -HT1 /2 width=2/
- ]
-]
-qed.
-