proposition: Lemma Equiv_add : forall n k x m', ~In k n -> Equiv eq (add k x n) m' -> exists x', eq x x' /\ Add k x' (remove k m') m'.
proof: Proof. intros n k x m' hk [h1 h2]. assert (In k (add k x n)). rewrite add_in_iff. auto with ordered_type. rewrite h1 in H. destruct H as [x']. exists x'. split. apply h2 with k. rewrite add_mapsto_iff. auto with ordered_type. hyp. intro l. rewrite add_o. rewrite remove_o. destruct (eq_dec k l). rewrite <- e. rewrite <- find_mapsto_iff. hyp. refl. Qed.
imports: Coq(FMaps FSetInterface) CoLoR(LogicUtil RelUtil BoolUtil ListUtil FSetUtil)