proposition: Lemma typed'_iter n (x y: traces') i: typed' n n x -> typed' n n y -> typed' n n (traces_iter y x i).
proof: Proof. intros Hx Hy. induction i. assumption. eapply typed'_dot; eassumption. Qed.
imports: prop monoid positives comparisons