proposition: Lemma rel_on_nat_intro i j a b : Dom[i] = Some a -> Dom[j] = Some b -> R a b -> rel_on_nat R i j.
proof: Proof. intros. unfold rel_on_nat. rewrite H, H0. exact H1. Qed.
imports: CoLoR(ListUtil SCC ListExtras Path Iter AdjMat RelSub LogicUtil ListNodup RelUtil BoundNat)