proposition: Lemma traces_dot1x x: traces_dot tt tt tt (traces_one tt) x ≡ x.
proof: Proof. intro w. split. intros [u Hu [v Hv E]]. destruct u as [?|]. 2: elim Hu. inversion E; subst; assumption. intro Hw. exists (tnil (thead w)). reflexivity. exists w. assumption. apply tapp_nil_x. Qed.
imports: prop monoid positives comparisons