fact: Definition Inv_solved_part pb := forall x, match find X.eq_bool x pb.(solved_part) with | Some (Var _) => is_a_solved_var x pb = true | _ => True 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)