proposition: Lemma rel_on_dom_intro i j a b : find_first (eq a) (eq_dec a) Dom = Some i -> find_first (eq b) (eq_dec b) Dom = Some j -> S i j -> rel_on_dom S a b.
proof: Proof. intros. unfold rel_on_dom. rewrite H, H0. exact H1. Qed.
imports: CoLoR(ListUtil SCC ListExtras Path Iter AdjMat RelSub LogicUtil ListNodup RelUtil BoundNat)