fact: Definition phi1 pb := VSet.cardinal (VSet.filter (fun v : variable => negb (is_a_solved_var v pb)) (VSet.union (set_of_variables_in_unsolved_part pb.(unsolved_part)) (VSet.union (domain_of_subst pb.(solved_part)) (set_of_variables_in_range_of_subst pb.(solved_part)))) (VSet_compat pb)).
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)