proposition: Lemma psi_nf : forall t, nf (one_step R) t -> psi t = t.
proof: Proof. intros t nf_t; destruct (psi_char t) as [[H1 H2] | P]; trivial. assert False; [idtac | contradiction]. apply (Psi_not_nf _ _ P nf_t). Qed.
imports: Coq(List Relations Wellfounded Arith) CoLoR(closure more_list weaved_relation term equational_theory_spec rwr_strategies dp rpo)