proposition: Lemma Psi_not_refl : forall t, Psi t t -> False.
proof: Proof. intro t; pattern t; apply term_rec3; clear t. intros v P; assert False; [idtac | contradiction]. apply (Psi_not_nf (Var v) (Var v)); trivial. apply nf_var. intros f l IHl P; inversion P as [u v H Acc_u H3 | f' ll H K H1 H2]; clear P; subst. apply (@cycle_not_acc _ (P_step R (inner R)) (Term f l)). apply P_at_top; trivial. apply wf_inner. destruct K as [s [t [st_in_ll not_nf_t]]]. assert (s_eq_t : s = t). clear H not_nf_t IHl; induction ll as [ | [u v] ll]. contradiction. simpl in st_in_ll; destruct st_in_ll as [st_eq_uv | st_in_ll]. injection st_eq_uv; clear st_eq_uv; intros; subst; injection H2; clear H2; intros; subst; trivial. apply IHll; trivial; injection H2; clear H2; intros; trivial. destruct (H s t st_in_ll) as [P | [_ nf_t]]. subst s; apply (IHl t); trivial. rewrite in_map_iff; exists (t,t); split; trivial. apply not_nf_t; trivial. Qed.
imports: Coq(List Relations Wellfounded Arith) CoLoR(closure more_list weaved_relation term equational_theory_spec rwr_strategies dp rpo)