proposition: Lemma SN_notNT : forall x, SN R x -> ~NT R x.
proof: Proof. intros y hy [f [h0 hf]]. cut (forall i, ~SN R (f i)). intro h. apply (h 0). rewrite h0. hyp. cut (forall x, SN R x -> ~(exists i, x = f i)). intros h i hi. eapply h. apply hi. exists i. refl. induction 1. intros [i hi]. subst. eapply H0. apply hf. exists (S i). refl. Qed.
imports: Coq(Morphisms List Basics Lia Wellfounded) CoLoR(LogicUtil RelUtil)