proposition: Lemma P_acc_subterms : forall R P, (forall x t, ~ (R t (Var x))) -> forall f l, (forall t, In t l -> Acc (P_step R P) t) -> constructor R f -> Acc (P_step R P) (Term f l).
proof: Proof. intros R P HR f l Acc_l Cf'; inversion Cf' as [f' Cf]; clear Cf'; subst f'. rewrite acc_one_step_list in Acc_l. pattern l; refine (@Acc_ind _ (one_step_list (P_step R P)) _ _ l Acc_l). clear l Acc_l; intros l Acc_l IH. apply Acc_intro. intros t H; inversion H as [t' s Hnf H' | f' l1 l2 H']; subst. inversion H' as [t1 t2 sigma H'' H3 H''']; subst; destruct t2 as [x2 | f2 l2]. absurd (R t1 (Var x2)); trivial; apply HR. simpl in H'''; injection H'''; clear H'''; intros; subst; absurd (R t1 (Term f l2)); trivial; apply Cf. apply IH. generalize l2 l H'. intro k; induction k as [ | s k]; intros k' K; inversion K; subst. left; trivial. right; trivial. Qed.
imports: Coq(List Relations Wellfounded Arith) CoLoR(closure decidable_set more_list weaved_relation term_spec equational_theory_spec dp rpo)