proposition: Lemma dom_change x y : rel_on_dom (rel_on_nat R) x y <-> R x y.
proof: Proof. intros; split; intro. ded (rel_on_dom_elim H). repeat destruct H0; destruct H1. unfold rel_on_nat in H0. rewrite H1, H2 in H0; auto. unfold is_restricted in restriction. ded (restriction H); destruct H0. ded (eq_In_find_first eq_dec H0); ded (eq_In_find_first eq_dec H1). destruct H2; destruct H2; destruct H3; destruct H3. unfold rel_on_dom. rewrite H2, H3. unfold rel_on_nat. rewrite H4, H5; auto. Qed.
imports: CoLoR(ListUtil SCC ListExtras Path Iter AdjMat RelSub LogicUtil ListNodup RelUtil BoundNat)