proposition: Lemma is_empty_1 m : Empty m -> is_empty m = true.
proof: Proof. unfold Empty; rewrite is_empty_spec. setoid_rewrite <- find_spec. intros H x. specialize (H x). destruct (find x m) as [e|]; trivial. now destruct (H e). Qed.
imports: Coq(Bool Equalities Orders OrdersFacts OrdersLists) Coq(Morphisms Permutation SetoidPermutation) MMaps(Utils Comparisons Interface)