proposition: Lemma Psi_not_nf : forall t s, Psi s t -> nf (one_step R) t -> False.
proof: Proof. intros t; pattern t; apply term_rec3; clear t. intros v s P; inversion P as [ss tt H K | g ll H K]; subst. intro H'; unfold nf in H'; apply (H' s); apply at_top; trivial. intros f l IHl s P; inversion P as [ss tt H K | g ll H K]; clear P; subst. intro H'; unfold nf in H'; apply (H' s); apply at_top; trivial. destruct K as [s [t [st_in_ll P]]]. intro H'; apply P; apply (nf_one_step_subterm _ _ H'). simpl; rewrite in_map_iff; exists (s,t); split; trivial. Qed.
imports: Coq(List Relations Wellfounded Arith) CoLoR(closure more_list weaved_relation term equational_theory_spec rwr_strategies dp rpo)