fact: Definition shifted_active_in_list shift f l (s : term) := exists i, In (shift + i) (mu f) /\ nth_error l i = Some s.
imports: Coq(List Relations Wellfounded Arith) CoLoR(closure decidable_set more_list weaved_relation term_spec equational_theory_spec dp rpo)