proposition: Lemma rel_set_fold_add_edge_ext : forall x s g0 a b, rel (XSet.fold (add_edge x) s g0) a b <-> succ x s a b \/ rel g0 a b.
proof: Proof. split; intro h. apply rel_set_fold_add_edge in h. hyp. apply rel_set_fold_add_edge. hyp. Qed.
imports: Coq(OrderedType) CoLoR(ListUtil FSetUtil FMapUtil RelUtil LogicUtil)