proposition: Lemma remove_mapsto_iff m x y e : MapsTo y e (remove x m) <-> ~K.eq x y /\ MapsTo y e m.
proof: Proof. split; [split|destruct 1]. - intro E. revert H. now rewrite <-E, <- find_spec, remove_spec1. - now apply remove_3 with x. - now apply remove_2. Qed.
imports: Coq(Bool Equalities Orders OrdersFacts OrdersLists) Coq(Morphisms Permutation SetoidPermutation) MMaps(Utils Comparisons Interface)