fact: Fixpoint actives f n l : list term := match l with | nil => nil | t :: l => if mem_bool Nat.eqb n (mu f) then t :: (actives f (S n) l) else (actives f (S n) l) end.
imports: Coq(List Relations Wellfounded Arith) CoLoR(closure decidable_set more_list weaved_relation term_spec equational_theory_spec dp rpo)