∀ {assignment assignment_1 : Array (Bool × ℕ)},
  Lean.Elab.Tactic.BVDecide.External.SolverResult.sat assignment =
      Lean.Elab.Tactic.BVDecide.External.SolverResult.sat assignment_1 →
    assignment = assignment_1