lemma tpssa_tpss: ∀L,T1,T2,d,e. L ⊢ T1 ▶▶* [d, e] T2 → L ⊢ T1 ▶* [d, e] T2.
#L #T1 #T2 #d #e #H elim H -L -T1 -T2 -d -e // /2 width=6/
lemma tpssa_tpss: ∀L,T1,T2,d,e. L ⊢ T1 ▶▶* [d, e] T2 → L ⊢ T1 ▶* [d, e] T2.
#L #T1 #T2 #d #e #H elim H -L -T1 -T2 -d -e // /2 width=6/