proposition: Lemma SN_path : forall n x, (forall y l, length l = n -> path R x y l -> SN R y) -> SN R x.
proof: Proof. intros. apply SN_iter with n. apply SN_intro. intros. apply (SN_incl (R!)). apply iter_tc. apply SN_tc. ded (iter_path H0). do 2 destruct H1. subst n. apply H with x0. refl. hyp. Qed.
imports: Coq(Morphisms List Basics Lia Wellfounded) CoLoR(LogicUtil RelUtil) CoLoR(Iter) CoLoR(Path)