proposition: Lemma psi_char : forall t, (psi t = t /\ nf (one_step R) t) \/ (Psi (psi t) t).
proof: Proof. intros t; unfold psi. destruct (dec_nf (one_step R) (compute_red rule_list) (compute_red_is_correct rule_list Rreg' R Req) t). left; split; trivial. right; destruct (Psi_def t n) as [t' P]; trivial. Qed.
imports: Coq(List Relations Wellfounded Arith) CoLoR(closure more_list weaved_relation term equational_theory_spec rwr_strategies dp rpo)