fact: Definition rel_on_nat (R : relation A) i j := match Dom[i] with | None => False | Some a => match Dom[j] with | None => False | Some b => R a b end end.
imports: CoLoR(ListUtil SCC ListExtras Path Iter AdjMat RelSub LogicUtil ListNodup RelUtil BoundNat)