proposition: Lemma not_in_mapsto_iff : ∀ elt k (m : M.t elt), ~ M.In (elt:=elt) k m <-> ∀ e, ~ M.MapsTo (elt:=elt) k e m.
proof: Proof. split; intros; unfold not; intros. apply H. apply in_mapsto_iff. exists e; assumption. apply (proj1 (in_mapsto_iff _ _ _)) in H0. destruct H0. apply (H x); assumption. Qed.
imports: Coq.Unicode.Utf8 Coq.FSets.FMapFacts