proposition: Lemma rel_list_fold_left_add_edge_list : forall l g, fold_left add_edge_list l g == fold_left add_edge_list l empty U g.
proof: Proof. induction l; simpl; intro g. rewrite rel_empty, R.union_empty_l. refl. rewrite IHl. rewrite (IHl (add_edge_list empty a)). do 2 rewrite rel_add_edge_list. destruct (f a) as [[x m]|]; rewrite rel_empty, R.union_empty_r. rewrite R.union_assoc. refl. refl. Qed.
imports: Coq(OrderedType) CoLoR(RelUtil LogicUtil BoolUtil FGraph)