proposition: Lemma rel_add_edge_list : forall g a, add_edge_list g a == match f a with | None => g | Some (x,l) => succ_list x l U g end.
proof: Proof. intros g a. unfold add_edge_list. destruct (f a) as [[x l]|]. apply rel_list_fold_left_add_edge. refl. Qed.
imports: Coq(OrderedType) CoLoR(RelUtil LogicUtil BoolUtil FGraph)