fact: Definition Inv_solved_part_e e := match e with | Normal _ pb => Inv_solved_part pb | Not_appliable _ pb => pb.(unsolved_part) = nil | No_solution _ => 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)