fact: Definition nb_var_eq_of_unsolved_part pb := list_size (fun s_t => match s_t with (s,t) => match s, t with | Var _, _ => 1 | _ , Var _ => 1 | _, _ => 0 end end) pb.(unsolved_part).
imports: Coq(Arith Wf_nat Wellfounded List Multiset Relations) CoLoR(closure decidable_set ordered_set more_list list_permut list_set list_sort dickson term_spec term)