proposition: Lemma mapsto_dec : ∀ elt k e (m : M.t elt), (∀ x y : elt, {x = y} + {x <> y}) -> { M.MapsTo k e m } + { ~ M.MapsTo k e m }.
proof: Proof. intros. destruct (M.find k m) eqn:?. apply F.find_mapsto_iff in Heqo. destruct (X e e0); subst. left; assumption. right; unfold not; intros. pose proof (F.MapsTo_fun H Heqo). contradiction. apply F.not_find_in_iff in Heqo. right. apply not_in_mapsto_iff. assumption. Qed.
imports: Coq.Unicode.Utf8 Coq.FSets.FMapFacts