proposition: Lemma rel_add : forall x g s, ~In x g -> rel (add x s g) == succ x s U g.
proof: Proof. intros x g s n. rewrite rel_eq; intros a b. unfold Relation_Operators.union. split. intros [t [t1 t2]]. rewrite add_o in t1. destruct (eq_dec x a). inversion t1. subst t. firstorder auto with crelations. right. exists t. tauto. intros [ab|ab]. exists s. unfold succ in ab. split_all. rewrite add_o. destruct (eq_dec x a). refl. absurd (eq x a); hyp. destruct ab as [t [t1 t2]]. exists t. split_all. rewrite add_o. destruct (eq_dec x a). 2: hyp. absurd (In x g). hyp. rewrite e. exists t. change (MapsTo a t g). rewrite find_mapsto_iff. hyp. Qed.
imports: Coq(OrderedType) CoLoR(ListUtil FSetUtil FMapUtil RelUtil LogicUtil)