proposition: Lemma map_mapsto_iff {elt elt'} m x b (f : elt -> elt') : MapsTo x b (map f m) <-> exists a, b = f a /\ MapsTo x a m.
proof: Proof. rewrite <-find_spec, map_find. setoid_rewrite <- find_spec. destruct (find x m); simpl; split. - injection 1. now exists e. - intros (a,(->,H)). now injection H as ->. - discriminate. - intros (a,(_,H)); discriminate. Qed.
imports: Coq(Bool Equalities Orders OrdersFacts OrdersLists) Coq(Morphisms Permutation SetoidPermutation) MMaps(Utils Comparisons Interface)