proposition: Lemma map_psi : forall f l, psi (Term f l) = Term f (map psi l) \/ (P_step R (inner R) (psi (Term f l)) (Term f (map psi l)) /\ inner R (Term f (map psi l))).
proof: Proof. intros f l; destruct (psi_char (Term f l)) as [[H1 H2] | P]. left; rewrite (psi_nf (Term f l)); trivial. apply (f_equal (fun l => Term f l)). pattern l at 1; rewrite <- map_id; apply map_eq. intros s s_in_l; rewrite psi_nf; trivial. apply nf_one_step_subterm with (Term f l); trivial. inversion P as [s t H K | f' ll H K]; clear P; subst. right; replace (Term f (map psi l)) with (Term f l). split; trivial; apply P_at_top; trivial. apply (f_equal (fun l => Term f l)). pattern l at 1; rewrite <- map_id; apply map_eq. intros s s_in_l; rewrite psi_nf; trivial. apply K; trivial. left; apply (f_equal (fun l => Term f l)). rewrite map_map; apply map_eq. intros [s t] st_in_ll; simpl. destruct (H _ _ st_in_ll) as [H2 | [H2 nf_t]]. rewrite (Psi_psi _ _ H2); trivial. rewrite psi_nf; trivial. Qed.
imports: Coq(List Relations Wellfounded Arith) CoLoR(closure more_list weaved_relation term equational_theory_spec rwr_strategies dp rpo)