proposition: Lemma remove_in_iff m x y : In y (remove x m) <-> ~K.eq x y /\ In y m.
proof: Proof. unfold In; split; [ intros (e,H) | intros (E,(e,H)) ]. - apply remove_mapsto_iff in H. destruct H; split; trivial. now exists e. - exists e. now apply remove_2. Qed.
imports: Coq(Bool Equalities Orders OrdersFacts OrdersLists) Coq(Morphisms Permutation SetoidPermutation) MMaps(Utils Comparisons Interface)