proposition: Lemma Psi_sim_inner : forall t s, P_step R (inner R) s t -> refl_trans_clos (one_step R) (psi s) (psi t).
proof: Proof. intro t; pattern t; apply term_rec3; clear t. intros v s H; apply False_rect. inversion H as [t1 t2 H' | f' l1 l2 H']; clear H; subst. apply (nf_var v s); apply at_top; trivial. intros f l IHl s H; inversion H as [t1 t2 H' | f' l1 l2 H']; clear H; subst. destruct (Psi_sim_inner_at_top _ _ H0 H') as [H1 | H1]. left; trivial. right; trivial. destruct (P_step_in_list _ _ _ _ H') as [t [s [k1 [k2 [H1 [H2 H3]]]]]]. destruct (psi_char (Term f l)) as [[K1 K2] | P]. apply False_rect. rewrite one_step_nf_inner_step_nf in K2. apply (K2 (Term f l2)); apply P_in_context; trivial. apply Rvar. inversion P as [ss tt H K | g ll H4 K]; clear P. subst ss tt. assert False; [idtac | contradiction]. refine (K t _ s _). simpl; subst l; apply in_or_app; right; left; trivial. apply P_step_one_step with (inner R); trivial. subst g. assert (H6 : map (fst (A:=term) (B:=term)) ll = map psi l). rewrite <- H5; clear K H5 H. induction ll as [ | [u v] ll]; trivial. simpl; rewrite <- IHll. apply (f_equal (fun t => t :: map (fst (A:=term) (B:=term)) ll)). destruct (H4 _ _ (or_introl _ (eq_refl _))) as [H5 | [H5 H6]]. apply Psi_unique with v; trivial. apply psi_not_nf; intro H6; apply (Psi_not_nf v u); trivial. rewrite psi_nf; trivial. intros; apply H4; right; trivial. rewrite H6 in *. clear H4 H5 H6; rename H into H4. destruct (map_psi f l2) as [H5 | [H5 H5']]. rewrite H4; rewrite H5. assert (t_in_k : In t (k1 ++ t :: k2)). apply in_or_app; right; left; trivial. rewrite <- H2 in t_in_k. rewrite <- H4. rewrite H2, H3; do 2 rewrite map_app; simpl. assert (IH' := IHl _ t_in_k _ H1); inversion IH' as [x | ps pt H6]. left. right; apply context_in; assumption. assert (t_in_k : In t (k1 ++ t :: k2)). apply in_or_app; right; left; trivial. rewrite <- H2 in t_in_k. apply refl_trans_clos_is_trans with (Term f (map psi l2)). right; left; apply P_step_one_step with (inner R); trivial. rewrite H2, H3, map_app, map_app; simpl. assert (IH':= IHl _ t_in_k _ H1); inversion IH' as [x | ps pt H6]. left. right; apply context_in; assumption. Qed.
imports: Coq(List Relations Wellfounded Arith) CoLoR(closure more_list weaved_relation term equational_theory_spec rwr_strategies dp rpo)