lemma ltpss_tpss_conf: ∀L1,T1,T2,d,e. L1 ⊢ T1 [d, e] ≫* T2 →
∀L2,ds,es. L1 [ds, es] ≫* L2 →
∃∃T. L2 ⊢ T1 [d, e] ≫* T & L1 ⊢ T2 [ds, es] ≫* T.
#L1 #T1 #T2 #d #e #HT12 #L2 #ds #es #H @(ltpss_ind … H) -L2
lemma ltpss_tpss_conf: ∀L1,T1,T2,d,e. L1 ⊢ T1 [d, e] ≫* T2 →
∀L2,ds,es. L1 [ds, es] ≫* L2 →
∃∃T. L2 ⊢ T1 [d, e] ≫* T & L1 ⊢ T2 [ds, es] ≫* T.
#L1 #T1 #T2 #d #e #HT12 #L2 #ds #es #H @(ltpss_ind … H) -L2