proposition: Lemma remove_3 : MapsTo y e (remove x m) -> MapsTo y e m.
proof: Proof. unfold MapsTo. destruct (E.eq_dec x y). - subst. rewrite grs; intros; discriminate. - rewrite gro; auto. Qed.
imports: Bool OrderedType ZArith OrderedType OrderedTypeEx FMapInterface