proposition: Lemma measure_mempty {B} `{Monoid B} : bin_measure mempty = 0.
proof: Proof. assert (forall m n, n = n + m -> m = 0) by (induction n; simpl; eauto). eapply H0. etransitivity. - eapply (mappend_measure mempty mempty). - rewrite mempty_left; reflexivity. Qed.