proposition: Lemma dom_change_tc x y : rel_on_dom (rel_on_nat R !) x y <-> R! x y.
proof: Proof. split; intros. ded (rel_on_dom_elim2 H); do 3 destruct H0. ded (tc_iter H0); unfold Iter in *; unfold Iter_ge in *. destruct H2 as [n]. destruct H2; destruct H1. eapply (iter_tc R n); rewrite <- dom_change_iter. unfold rel_on_dom; rewrite H1, H4; trivial. ded (tc_iter H); unfold Iter in *; unfold Iter_ge in *. destruct H0 as [n]; destruct H0. rewrite <- dom_change_iter in H1. 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 *. ded (iter_tc (rel_on_nat R) n); auto. Qed.
imports: CoLoR(ListUtil SCC ListExtras Path Iter AdjMat RelSub LogicUtil ListNodup RelUtil BoundNat)