proposition: Lemma rel_list_fold_left_add_edge : forall x l g0, fold_left (add_edge' x) l g0 == succ_list x l U g0.
proof: Proof. induction l; simpl; intro g. rewrite succ_list_nil, R.union_empty_l. refl. rewrite IHl, succ_list_cons. unfold add_edge'. rewrite rel_add_edge. rewrite union_commut with (R:=rel g). rewrite <- R.union_assoc. rewrite union_commut with (R:=id x a). refl. Qed.
imports: Coq(OrderedType) CoLoR(ListUtil FSetUtil FMapUtil RelUtil LogicUtil)