proposition: Lemma Psi_psi : forall s t, Psi s t -> psi t = s.
proof: Proof. intros s t P; apply Psi_unique with t; trivial. apply psi_not_nf. intro H; apply (Psi_not_nf t s); trivial. Qed.
imports: Coq(List Relations Wellfounded Arith) CoLoR(closure more_list weaved_relation term equational_theory_spec rwr_strategies dp rpo)