proposition: Lemma in_mapsto_iff : ∀ elt k (m : M.t elt), M.In (elt:=elt) k m <-> exists e, M.MapsTo (elt:=elt) k e m.
proof: Proof. split; intros. apply F.mem_in_iff in H. rewrite F.mem_find_b in H. destruct (M.find (elt:=elt) k m) eqn:Heqe. exists e. apply F.find_mapsto_iff. assumption. discriminate. apply F.mem_in_iff. rewrite F.mem_find_b. destruct H. apply F.find_mapsto_iff in H. rewrite H. reflexivity. Qed.
imports: Coq.Unicode.Utf8 Coq.FSets.FMapFacts