proposition: Lemma traces_dotx1 x: traces_dot tt tt tt x (traces_one tt) ≡ x.
proof: Proof. intro w. split. intros [u Hu [[|] Hv E]]. 2: elim Hv. now apply tapp_x_nil_eq in E as [? ->]. intro Hw. exists w. assumption. exists (tnil (ttail w)). reflexivity. apply tapp_x_nil. Qed.
imports: prop monoid positives comparisons