proposition: Lemma cardinal_Empty m : Empty m <-> cardinal m = 0.
proof: Proof. intros. rewrite cardinal_1, bindings_Empty. destruct (bindings m); intuition; discriminate. Qed.
imports: Coq(Bool Equalities Orders OrdersFacts OrdersLists) Coq(Morphisms Permutation SetoidPermutation) MMaps(Utils Comparisons Interface)