proposition: Lemma Empty_alt : forall m, Empty m <-> forall a, find a m = None.
proof: Proof. unfold Empty, MapsTo. intuition. - generalize (H a). destruct (find a m); intuition. elim (H0 a0); auto. - rewrite H in H0; discriminate. Qed.
imports: Bool OrderedType ZArith OrderedType OrderedTypeEx FMapInterface