proposition: Lemma rel_on_nat_dec x y : {rel_on_nat R x y}+{~rel_on_nat R x y}.
proof: Proof. unfold rel_on_nat. destruct (Dom[x]). destruct (Dom[y]). apply Rdec. tauto. tauto. Defined.
imports: CoLoR(ListUtil SCC ListExtras Path Iter AdjMat RelSub LogicUtil ListNodup RelUtil BoundNat)