proposition: Lemma in_mapsto_iffT : ∀ elt k (m : M.t elt), CRelationClasses.iffT (M.In (elt:=elt) k m) { e : elt & 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 X. apply F.find_mapsto_iff in m0. rewrite m0. reflexivity. Defined.
imports: Coq.Unicode.Utf8 Coq.FSets.FMapFacts