proposition: Lemma add_mapsto_iffT : ∀ elt m x y (e e' : elt), CRelationClasses.iffT (M.MapsTo y e' (M.add x e m)) ((E.eq x y * (e=e'))%type + ((~E.eq x y) * M.MapsTo y e' m)).
proof: Proof. split; intros. apply F.find_mapsto_iff in H. rewrite F.add_o in H. destruct (F.eq_dec x y). inversion_clear H. left; auto. right. split; auto. apply F.find_mapsto_iff; assumption. apply F.find_mapsto_iff. rewrite F.add_o. destruct H. destruct p. destruct (F.eq_dec x y). rewrite e1; reflexivity. rewrite e0 in n. contradiction n. reflexivity. destruct p. destruct (F.eq_dec x y). rewrite e0 in n. contradiction n. reflexivity. apply F.find_mapsto_iff. assumption. Defined.
imports: Coq.Unicode.Utf8 Coq.FSets.FMapFacts