fact: Definition active_in_list f l (s : term) := shifted_active_in_list 0 f l s.
imports: Coq(List Relations Wellfounded Arith) CoLoR(closure decidable_set more_list weaved_relation term_spec equational_theory_spec dp rpo)