proposition: Lemma Equal_mapsto_iff : forall m1 m2 : t elt, Equal m1 m2 <-> (forall k e, MapsTo k e m1 <-> MapsTo k e m2).
proof: Proof. intros m1 m2. split; [intros Heq k e|intros Hiff]. - rewrite 2 find_mapsto_iff, Heq. split; auto. - intro k. rewrite eq_option_alt. intro e. rewrite <- 2 find_mapsto_iff; auto. Qed.
imports: Bool DecidableType DecidableTypeEx OrderedType Morphisms FMapInterface