proposition: Lemma rel_on_dom_elim2 x y : rel_on_dom S x y -> exists a, exists b, S a b /\ find_first (eq x) (eq_dec x) Dom = Some a /\ find_first (eq y) (eq_dec y) Dom = Some b.
proof: Proof. intros; unfold rel_on_dom in H. assert (exists a, find_first (eq x) (eq_dec x) Dom =Some a). destruct (find_first (eq x) (eq_dec x) Dom ); try tauto. exists n; auto. destruct H0; subst. rewrite H0 in H. assert (exists b,find_first (eq y) (eq_dec y) Dom =Some b). destruct (find_first (eq y) (eq_dec y) Dom ); try tauto. exists n; auto. destruct H1; subst; rewrite H1 in H. ded (eq_find_first_exact H1). ded (eq_find_first_exact H0). exists x0; exists x1; intuition; auto. Qed.
imports: CoLoR(ListUtil SCC ListExtras Path Iter AdjMat RelSub LogicUtil ListNodup RelUtil BoundNat)