proposition: Lemma rel_trans_clos_list : forall l, trans_clos_list l == fold_left add_edge_list l empty!.
proof: Proof. intro l. unfold trans_clos_list. rewrite rel_list_fold_left_trans_add_edge_list. refl. apply transitive_empty. Qed.
imports: Coq(OrderedType) CoLoR(RelUtil LogicUtil BoolUtil FGraph)