proposition: Lemma restrict_iter n (x y: traces') i: typed' n n x -> typed' n n y -> restrict n n (traces_iter y x i) ≡ ttraces_iter (restrict n n y) (restrict n n x) i.
proof: Proof. intros Hx Hy. induction i. simpl. now unfold ttraces_weq. simpl. setoid_rewrite restrict_dot. now setoid_rewrite IHi. assumption. now apply typed'_iter. Qed.
imports: prop monoid positives comparisons