fact: Definition well_formed_pb pb := (forall t1 t2, In (t1,t2) pb.(unsolved_part) -> well_formed_cf t1 /\ well_formed_cf t2) /\ (forall v, match (find X.eq_bool v pb.(solved_part)) with | None => True | Some t => well_formed_cf t end) /\ (forall v, match (find X.eq_bool v pb.(partly_solved_part)) with | None => True | Some pst => match arity pst.(head_symb) with | AC => well_formed_cf pst.(closed_term) /\ match pst.(closed_term) with | Var _ => True | Term f _ => pst.(head_symb)<>f end | _ => False end end) /\ (forall v, nb_occ X.eq_bool v (solved_part pb) + nb_occ X.eq_bool v (partly_solved_part pb) <= 1) /\ well_sorted_partly_solved_part (partly_solved_part pb) /\ (forall v p, find X.eq_bool v (partly_solved_part pb) = Some p -> occurs_in_pb (new_var p) pb).
imports: Coq(Arith List) CoLoR(more_list list_sort term_spec ac cf_eq_ac)