proposition: Lemma Equal_cardinal : forall m m' : t elt, Equal m m' -> cardinal m = cardinal m'.
proof: Proof. intros; do 2 rewrite cardinal_fold. apply fold_Equal with (eqA:=eq); compute; auto. Qed.
imports: Bool DecidableType DecidableTypeEx OrderedType Morphisms FMapInterface