lapply (IHV … HT12) -IHV -HT12 #HT12 @step /2 width=5/ (**) (* /3 width=5/ is too slow *)
]
qed.
lemma tpss_flat: ∀L,I,V1,V2,T1,T2,d,e.
L ⊢ V1 [d, e] ▶ * V2 → L ⊢ T1 [d, e] ▶* T2 →
lapply (IHV … HT12) -IHV -HT12 #HT12 @step /2 width=5/ (**) (* /3 width=5/ is too slow *)
]
qed.
lemma tpss_flat: ∀L,I,V1,V2,T1,T2,d,e.
L ⊢ V1 [d, e] ▶ * V2 → L ⊢ T1 [d, e] ▶* T2 →