fact: Definition trans_add_edge x y g := if XSet.mem y (succs x g) then g else let ysy := XSet.add y (succs y g) in fold (add_pred x ysy) g (XSet.fold (add_edge x) ysy g).
imports: Coq(OrderedType) CoLoR(RelUtil LogicUtil BoolUtil FGraph)