fact: Parameter solve_is_complete : forall pb, well_formed_pb pb -> forall sigma, is_well_formed_sol pb sigma -> match pb.(unsolved_part) with | nil => True | _ :: _ => exists pb', In pb' (solve pb) /\ is_well_formed_sol pb' sigma end.
imports: Coq(Arith List) CoLoR(more_list list_sort term_spec ac cf_eq_ac matching_sound)