proposition: Lemma P_acc_subterms_3 : forall R P p t s, Acc (P_step R P) t -> subterm_at_pos t p = Some s -> Acc (P_step R P) s.
proof: Proof. intros R P p; induction p as [ | i p]; intros t s Acc_t H; simpl in H. injection H; intro; subst; trivial. destruct t as [ x | f l]. discriminate. assert (H' := nth_error_ok_in i l); destruct (nth_error l i) as [ s' | ]. generalize (H' _ (eq_refl _)); clear H'; intro s'_in_l. apply (IHp s'); trivial; apply (P_acc_subterms_1 R P (Term f l)); trivial. destruct s'_in_l as [l1 [l2 [_ H']]]; subst l; simpl; apply in_or_app; right; left; trivial. discriminate. Qed.
imports: Coq(List Relations Wellfounded Arith) CoLoR(closure decidable_set more_list weaved_relation term_spec equational_theory_spec dp rpo)