proposition: Lemma dom_change_transp x y : rel_on_dom (transp R) x y <-> transp (rel_on_dom R) x y.
proof: Proof. split; intros; unfold transp in *; unfold rel_on_dom in *; destruct (find_first (eq x) (eq_dec x) Dom); auto with *; destruct (find_first (eq y) (eq_dec y) Dom); auto with *. Qed.
imports: CoLoR(ListUtil SCC ListExtras Path Iter AdjMat RelSub LogicUtil ListNodup RelUtil BoundNat)