fact: Definition is_a_solution pb theta := (forall s t, In (s,t) pb.(unsolved_part) -> apply_subst theta s = apply_subst theta t) /\ (forall x, match find X.eq_bool x pb.(solved_part) with | Some x_val => apply_subst theta (Var x) = apply_subst theta x_val | None => 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)