proposition: Lemma context_acc_subterms_1 : forall R t s, Acc (C_step R) t -> active_direct_subterm s t -> Acc (C_step R) s.
proof: Proof. intros R t s Acc_t; generalize s; clear s; pattern t. refine (@Acc_ind _ (C_step R) _ _ 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 H as [i [H1 H2]]. destruct (nth_error_ok_in _ _ H2) as [l1 [l2 [L H'']]]; subst l. apply (IH (Term f (l1 ++ u :: l2))). apply C_in_context with i; trivial. subst i; revert H'; clear; induction l1 as [ | a1 l1]; intro H. left; assumption. right; apply IHl1; assumption. exists (length l1); split. subst; trivial. rewrite nth_error_at_pos; apply eq_refl. Qed.
imports: Coq(List Relations Wellfounded Arith) CoLoR(closure decidable_set more_list weaved_relation term_spec equational_theory_spec dp rpo)