proposition: Lemma is_empty_iff m : Empty m <-> is_empty m = true.
proof: Proof. split; [apply is_empty_1 | apply is_empty_2 ]. Qed.
imports: Coq(Bool Equalities Orders OrdersFacts OrdersLists) Coq(Morphisms Permutation SetoidPermutation) MMaps(Utils Comparisons Interface)