proposition: Lemma succ_add : forall x y s, succ x (XSet.add y s) == id x y U succ x s.
proof: Proof. intros x y s. apply rel_eq; intros a b. unfold Relation_Operators.union, succ, id. rewrite add_iff. firstorder auto with crelations. Qed.
imports: Coq(OrderedType) CoLoR(ListUtil FSetUtil FMapUtil RelUtil LogicUtil)