proposition: Lemma restrict_itr n (x: traces'): typed' n n x -> restrict n n (x^+) ≡ (restrict n n x)^+.
proof: Proof. intros Hx w. simpl. split. intros [H [i Hw]]. exists i. apply restrict_iter; trivial. now split. intros [i Hw]. split. eapply typed'_iter. 3: eassumption. now intros ? []. now intros ? []. exists i. eapply restrict_iter; eassumption. Qed.
imports: prop monoid positives comparisons