fact: Definition size_of_solved_part pb := list_size_mul _ (fun x => match find X.eq_bool x pb.(solved_part) with Some x_val => size x_val | None => 0 end) (VSet.support (domain_of_subst pb.(solved_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)