proposition: Lemma remove_2 m x y e : ~ K.eq x y -> MapsTo y e m -> MapsTo y e (remove x m).
proof: Proof. intro. now rewrite <- !find_spec, remove_spec2. Qed.
imports: Coq(Bool Equalities Orders OrdersFacts OrdersLists) Coq(Morphisms Permutation SetoidPermutation) MMaps(Utils Comparisons Interface)