proposition: Lemma acc_inner_acc : forall t, Acc (one_step R) t.
proof: Proof. intro t; pattern t; refine (well_founded_ind (wf_trans wf_inner) _ _ t); clear t. intros t IH; apply acc_psi_acc. destruct (psi_char t) as [[H3 H4] | H3]. rewrite H3; apply Acc_intro; intros s H. assert False; [idtac | contradiction]. apply (H4 _ H). apply IH; apply Psi_rwr; trivial. Qed.
imports: Coq(List Relations Wellfounded Arith) CoLoR(closure more_list weaved_relation term equational_theory_spec rwr_strategies dp rpo)