proposition: Lemma Psi_sim_inner_at_top : forall t s, axiom R s t -> inner R t -> refl_trans_clos (one_step R) (psi s) (psi t).
proof: Proof. intros t s H It; inversion H as [r l sigma H']; clear H; subst. destruct (psi_char (apply_subst sigma l)) as [[_ H] | P]. absurd (one_step R (apply_subst sigma r) (apply_subst sigma l)). intro H''; apply (H _ H''). apply at_top; apply instance; trivial. inversion P as [u v H Acc_u H3 | f' ll H K H1 H2]; clear P; subst. assert (H7 : psi (apply_subst sigma l) = apply_subst sigma r). apply (UIR (apply_subst sigma l)); trivial. apply instance; trivial. rewrite H7. destruct (psi_char (apply_subst sigma r)) as [[H1 H2] | P]. rewrite H1; left; split; trivial. right; apply trans_incl with (P_step R (inner R)). intros s t H6; apply P_step_one_step with (inner R); trivial. apply Psi_rwr; trivial. destruct K as [s [t [st_in_ll not_nf_t]]]. absurd (nf (one_step R) t); trivial. apply It; rewrite <- H2; simpl; rewrite in_map_iff; exists (s,t); split; trivial. Qed.
imports: Coq(List Relations Wellfounded Arith) CoLoR(closure more_list weaved_relation term equational_theory_spec rwr_strategies dp rpo)