proposition: Lemma cardinal_inv_2 m n : cardinal m = S n -> { p : key*elt | MapsTo (fst p) (snd p) m }.
proof: Proof. intros; rewrite M.cardinal_spec in *. generalize (bindings_mapsto_iff m). destruct (bindings m); try discriminate. exists p; auto. rewrite H0; destruct p; simpl; auto. constructor; compute; auto with map. Qed.
imports: Coq(Bool Equalities Orders OrdersFacts OrdersLists) Coq(Morphisms Permutation SetoidPermutation) MMaps(Utils Comparisons Interface)