proposition: Lemma rel_on_nat_elim a b : rel_on_nat R a b -> exists x, exists y, R x y /\ Dom [a] = Some x /\ Dom [b] = Some y.
proof: Proof. intros. unfold rel_on_nat in H. destruct (Dom[a]); destruct (Dom[b]); try discr; try tauto. exists a0; exists a1; intuition; auto. Qed.
imports: CoLoR(ListUtil SCC ListExtras Path Iter AdjMat RelSub LogicUtil ListNodup RelUtil BoundNat)