proposition: Lemma traces_dotA n m p q x y z: traces_dot n m q x (traces_dot m p q y z) ≡ traces_dot n p q (traces_dot n m p x y) z.
proof: Proof. intro w. simpl. split. intros [? ? [? [? ? [? ? E]] E']]. destruct (tapp_ass' E E') as (?&?&?). repeat eexists; eassumption. intros [? [? ? [? ? E]] [? ? E']]. destruct (tapp_ass E E') as (?&?&?). repeat eexists; eassumption. Qed.
imports: prop monoid positives comparisons