proposition: Lemma SN_iter : forall n x, SN (iter R n) x -> SN R x.
proof: Proof. induction n; intros. hyp. apply IHn. apply SN_iter_S'. hyp. Qed.
imports: Coq(Morphisms List Basics Lia Wellfounded) CoLoR(LogicUtil RelUtil) CoLoR(Iter)