proposition: Lemma restrict_dot n m p (x y: traces'): typed' n m x -> typed' m p y -> restrict n p (x ⋅ y) ≡ restrict n m x ⋅ restrict m p y.
proof: Proof. intros Hx Hy w; simpl. split. intros [Hw [u Hu [v Hv H]]]. repeat eexists; eauto. intros [u [Hu Hu'] [v [Hv Hv'] H]]. split. eapply tapp_typed; eassumption. repeat eexists; eassumption. Qed.
imports: prop monoid positives comparisons