lemma lstas_correct: ∀h,G,L,T1,T,d1. ⦃G, L⦄ ⊢ T1 •*[h, d1] T →
∀d2. ∃T2. ⦃G, L⦄ ⊢ T •*[h, d2] T2.
#h #G #L #T1 #T #d1 #H elim H -G -L -T1 -T -d1
lemma lstas_correct: ∀h,G,L,T1,T,d1. ⦃G, L⦄ ⊢ T1 •*[h, d1] T →
∀d2. ∃T2. ⦃G, L⦄ ⊢ T •*[h, d2] T2.
#h #G #L #T1 #T #d1 #H elim H -G -L -T1 -T -d1