fact: Definition is_rough_sol pb sigma := (forall t1 t2, In (t1,t2) pb.(unsolved_part) -> apply_cf_subst sigma t1 = t2) /\ (forall v, match find X.eq_bool v pb.(partly_solved_part) with | None => True | Some pst => let l := (apply_cf_subst sigma (Var pst.(new_var))) :: pst.(closed_term) :: nil in apply_cf_subst sigma (Var v) = Term pst.(head_symb) (quicksort (flatten pst.(head_symb) l)) end) /\ (forall v, match find X.eq_bool v pb.(solved_part) with | None => True | Some t => apply_cf_subst sigma (Var v) = t end).
imports: Coq(Arith List) CoLoR(more_list list_sort term_spec ac cf_eq_ac)