proposition: Lemma context_acc_subterms : forall R, (forall x t, ~ (R t (Var x))) -> forall f l, (forall t, active_in_list f l t -> Acc (C_step R) t) -> constructor R f -> Acc (C_step R) (Term f l).
proof: Proof. intros R HR f l Acc_l Cf'; inversion Cf' as [f' Cf]; clear Cf'; subst f'. assert (Acc_l' := Acc_C_step_acc_c_in_context _ _ _ Acc_l); clear Acc_l. induction Acc_l' as [l Acc_l IH]. apply Acc_intro. intros t H; inversion H as [t1 t2 H' | f' n 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. exists n; split; trivial. Qed.
imports: Coq(List Relations Wellfounded Arith) CoLoR(closure decidable_set more_list weaved_relation term_spec equational_theory_spec dp rpo)