proposition: Lemma dom_change_SCC x y : rel_on_dom (SCC (rel_on_nat R)) x y <-> SCC R x y.
proof: Proof. split; intros; unfold SCC in *. change (R! x y /\ transp (R!) x y). change (rel_on_dom (intersection (rel_on_nat R !) (transp (rel_on_nat R !))) x y) in H. rewrite dom_change_inter in H. destruct H; rewrite dom_change_transp in H0. unfold transp in *. rewrite dom_change_tc in *; auto with *. change (R! x y /\ transp (R!) x y) in H. change (rel_on_dom (intersection (rel_on_nat R !) (transp (rel_on_nat R !))) x y). rewrite dom_change_inter. destruct H; rewrite dom_change_transp. unfold transp in *. rewrite dom_change_tc; auto with *; rewrite dom_change_tc; auto with *. Qed.
imports: CoLoR(ListUtil SCC ListExtras Path Iter AdjMat RelSub LogicUtil ListNodup RelUtil BoundNat)