proposition: Lemma context_acc_subterms_2 : forall R t s, Acc (C_step R) t -> active_subterm s t -> Acc (C_step R) s.
proof: Proof. intros R t s Acc_t H. inversion H as [u | s' t' H']; clear H. assumption. subst. rewrite trans_clos_trans_clos_alt in H'. induction H' as [x y | x y z]. apply context_acc_subterms_1 with y; trivial. apply IHH'. apply context_acc_subterms_1 with z; trivial. Qed.
imports: Coq(List Relations Wellfounded Arith) CoLoR(closure decidable_set more_list weaved_relation term_spec equational_theory_spec dp rpo)