lemma lstas_split_aux: ∀h,G,L,T1,T2,l. ⦃G, L⦄ ⊢ T1 •*[h, l] T2 → ∀l1,l2. l = l1 + l2 →
∃∃T. ⦃G, L⦄ ⊢ T1 •*[h, l1] T & ⦃G, L⦄ ⊢ T •*[h, l2] T2.
#h #G #L #T1 #T2 #l #H elim H -G -L -T1 -T2 -l
lemma lstas_split_aux: ∀h,G,L,T1,T2,l. ⦃G, L⦄ ⊢ T1 •*[h, l] T2 → ∀l1,l2. l = l1 + l2 →
∃∃T. ⦃G, L⦄ ⊢ T1 •*[h, l1] T & ⦃G, L⦄ ⊢ T •*[h, l2] T2.
#h #G #L #T1 #T2 #l #H elim H -G -L -T1 -T2 -l