fact: Definition active_direct_subterm s t := match t with | Var _ => False | Term f l => active_in_list f l s end.
imports: Coq(List Relations Wellfounded Arith) CoLoR(closure decidable_set more_list weaved_relation term_spec equational_theory_spec dp rpo)