proposition: Lemma psi_not_nf : forall t, ~nf (one_step R) t -> Psi (psi t) t.
proof: Proof. intros t nf_t; destruct (psi_char t) as [[H1 H2] | P]; trivial. absurd (nf (one_step R) t); trivial. Qed.
imports: Coq(List Relations Wellfounded Arith) CoLoR(closure more_list weaved_relation term equational_theory_spec rwr_strategies dp rpo)