proposition: Lemma traces_dot_nil (L L': traces') a: (L⋅L')%ra (tnil a) <-> L (tnil a) /\ L' (tnil a).
proof: Proof. split. intros [h H [k K E]]. inversion E. subst. clear E. now split. intros [H H']. repeat eexists; eauto using tapp_nil_nil. Qed.
imports: prop monoid positives comparisons