proposition: Lemma P_acc_subterms_1 : forall R P t s, Acc (P_step R P) t -> direct_subterm s t -> Acc (P_step R P) s.
proof: Proof. intros R P t s Acc_t; generalize s; clear s; pattern t; refine (@Acc_ind _ (P_step R P) _ _ t Acc_t). clear t Acc_t; intros t Acc_t IH s H; destruct t as [ x | f l]; simpl in H. contradiction. apply Acc_intro; intros u H'; destruct (In_split _ _ H) as [l1 [l2 H'']]; subst l; apply (IH (Term f (l1 ++ u :: l2))). apply P_step_context_in; trivial. simpl; apply in_or_app; right; left; trivial. Qed.
imports: Coq(List Relations Wellfounded Arith) CoLoR(closure decidable_set more_list weaved_relation term_spec equational_theory_spec dp rpo)