(* Basic properties *********************************************************)
lemma ltpss_strap: ∀L1,L,L2,d,e.
L1 [d, e] ≫ L → L [d, e] ≫* L2 → L1 [d, e] ≫* L2.
(* Basic properties *********************************************************)
lemma ltpss_strap: ∀L1,L,L2,d,e.
L1 [d, e] ≫ L → L [d, e] ≫* L2 → L1 [d, e] ≫* L2.