proposition: Lemma acc_psi_acc_ooo : forall pt, Acc (one_step R) pt -> forall t, psi t = pt -> Acc ooo t.
proof: Proof. intros a Acc_a; generalize (acc_trans Acc_a); clear Acc_a; intro Acc_a. induction Acc_a as [a Acc_a IHa]. intros t H; subst a. generalize Acc_a IHa; clear Acc_a IHa; pattern t; refine (well_founded_ind (wf_trans wf_inner) _ _ t); clear t. intros t IH Acc_psi_t Acc_t. apply Acc_intro; intros s H. unfold ooo, oo, psi_id in *. unfold lex in H. revert H; generalize (eq_bool_ok (psi s) (psi t)); case (eq_bool (psi s) (psi t)); [intro psi_s_eq_psi_t | intro psi_s_diff_psi_t]. intro H; apply (IH s H); rewrite psi_s_eq_psi_t; trivial. intro H; apply Acc_t with (psi s); trivial. Qed.
imports: Coq(List Relations Wellfounded Arith) CoLoR(closure more_list weaved_relation term equational_theory_spec rwr_strategies dp rpo)