proposition: Lemma psi_inner_axiom : forall s t, inner R t -> axiom R s t -> psi t = s.
proof: Proof. intros s t H H'; destruct (psi_char t) as [[H1 H2] | P]. absurd (one_step R s t). intro H''; apply (H2 s H''). apply at_top; trivial. apply Psi_unique with t; trivial. apply Psi_at_top; trivial. Qed.
imports: Coq(List Relations Wellfounded Arith) CoLoR(closure more_list weaved_relation term equational_theory_spec rwr_strategies dp rpo)