fact: Definition rel_on_dom (S : relation nat) a b := match find_first (eq a) (eq_dec a) Dom with | None => False | Some p => match find_first (eq b) (eq_dec b) Dom with | None => False | Some q => S p q end end.
imports: CoLoR(ListUtil SCC ListExtras Path Iter AdjMat RelSub LogicUtil ListNodup RelUtil BoundNat)