proposition: Lemma Equiv_add_remove : forall n k x m', ~In k n -> Equiv eq (add k x n) m' -> Equiv eq n (remove k m').
proof: Proof. intros n k x m' hk [h1 h2]. split. intro l. rewrite remove_in_iff. intuition. apply hk. rewrite H0. hyp. rewrite <- h1. rewrite add_in_iff. auto. rewrite <- h1 in H1. rewrite add_in_iff in H1. intuition. intros l y z ly lz. assert (~E.eq k l). intro e. apply hk. exists y. change (MapsTo k y n). rewrite (MapsTo_iff _ _ e). hyp. apply h2 with l. rewrite add_mapsto_iff. right. intuition. rewrite remove_mapsto_iff in lz. intuition. Qed.
imports: Coq(FMaps FSetInterface) CoLoR(LogicUtil RelUtil BoolUtil ListUtil FSetUtil)