fact: Definition pb_weight pb := list_size (fun t1_t2 : term * term => match t1_t2 with | (t1,t2) => ac_size t1 + ac_size t2 end) (unsolved_part pb).
imports: Coq(Arith List) CoLoR(more_list list_sort term_spec ac cf_eq_ac matching)