fact: Definition compute_red : term -> list term := Fix wf_size (fun t => list term) F_compute_red.
imports: Coq(List Relations Wellfounded Arith Setoid) CoLoR(closure more_list weaved_relation dickson term_spec equational_theory_spec)