proposition: Lemma psi_subst : forall sigma tau, tau = map (fun xval => (@fst variable term xval, psi (@snd variable term xval))) sigma -> forall t, refl_trans_clos (P_step R (inner R)) (psi (apply_subst sigma t)) (apply_subst tau t).
proof: Proof. intros sigma tau H; assert (Hvar : forall v, apply_subst tau (Var v) = psi (apply_subst sigma (Var v))). intros v; simpl; subst tau. assert (H3 := @find_map _ X.eq_bool _ _ psi v sigma). destruct (find X.eq_bool v sigma) as [val | ]; rewrite H3; trivial. rewrite psi_nf; trivial; apply nf_var. intro t; pattern t; apply term_rec3; clear t. intros v; rewrite Hvar; left. intros f l IHl; simpl. destruct (map_psi f (map (apply_subst sigma) l)) as [H1 | [H1 H1']]. rewrite H1. assert (H2 : refl_trans_clos (one_step_list (P_step R (inner R))) (map psi (map (apply_subst sigma) l)) (map (apply_subst tau) l)). rewrite map_map; rewrite refl_trans_clos_one_step_list_refl_trans_clos_alt; trivial. inversion H2 as [l2 | l1 l2 K2]. left. right; apply P_general_context; trivial. assert (H2 : refl_trans_clos (one_step_list (P_step R (inner R))) (map psi (map (apply_subst sigma) l)) (map (apply_subst tau) l)). rewrite map_map; rewrite refl_trans_clos_one_step_list_refl_trans_clos_alt; trivial. inversion H2 as [l2 | l1 l2 K2]. right; apply t_step; trivial. right; apply trans_clos_is_trans with (Term f (map psi (map (apply_subst sigma) l))). apply t_step; trivial. apply P_general_context; trivial. Qed.
imports: Coq(List Relations Wellfounded Arith) CoLoR(closure more_list weaved_relation term equational_theory_spec rwr_strategies dp rpo)