proposition: Lemma IS_iter : forall R : relation A, (forall x, R x (f x)) -> IS R (iter a f).
proof: Proof. intros R hf. unfold IS. destruct i; simpl; apply hf. Qed.
imports: CoLoR(RelUtil NatUtil Path LeastNat LogicUtil ClassicUtil SN NotSN_IS SortUtil ListUtil) Coq(IndefiniteDescription)