fact: Definition is_a_solved_var x pb := match find X.eq_bool x pb.(solved_part) with | None => false | Some _ => andb (negb (mem_bool X.eq_bool x (VSet.support (set_of_variables_in_unsolved_part pb.(unsolved_part))))) (negb (mem_bool X.eq_bool x (VSet.support (set_of_variables_in_range_of_subst pb.(solved_part))))) end.
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)