proposition: Lemma add_mapsto_iff m x y e e' : MapsTo y e' (add x e m) <-> (K.eq x y /\ e=e') \/ (~K.eq x y /\ MapsTo y e' m).
proof: Proof. split. - intros H. destruct (K.eq_dec x y); [left|right]; split; trivial. + symmetry. apply (mapsto_fun H); auto with map. + now apply add_3 with x e. - destruct 1 as [(H,H')|(H,H')]; subst; auto with map. Qed.
imports: Coq(Bool Equalities Orders OrdersFacts OrdersLists) Coq(Morphisms Permutation SetoidPermutation) MMaps(Utils Comparisons Interface)