proposition: Lemma iter_preserve_restriction n : is_restricted (iter R n) Dom.
proof: Proof. induction n; try trivial. simpl; unfold is_restricted; unfold compose. intros; destruct H as [z]; destruct H. intuition. ded (restriction H); tauto. ded (IHn _ _ H0); tauto. Qed.
imports: CoLoR(ListUtil SCC ListExtras Path Iter AdjMat RelSub LogicUtil ListNodup RelUtil BoundNat)