proposition: Lemma rel_set_fold_add_edge : forall x s g0, XSet.fold (add_edge x) s g0 == succ x s U g0.
proof: Proof. intros x s g0. pattern (XSet.fold (add_edge x) s g0). apply XSetProps.fold_rec_weak; clear s. intros s t g st i. rewrite <- st. hyp. rewrite succ_empty. rewrite R.union_empty_l. refl. intros z g s nzs e. rewrite rel_add_edge. rewrite e. rewrite R.union_assoc. rewrite union_commut with (R:=rel g0). rewrite <- R.union_assoc. apply R.union_same. 2: refl. rewrite rel_eq; intros a b. unfold succ, Relation_Operators.union, id. rewrite add_iff, (eq_com b z). tauto. Qed.
imports: Coq(OrderedType) CoLoR(ListUtil FSetUtil FMapUtil RelUtil LogicUtil)