∀ {assumptions : Array Lean.Elab.Tactic.Omega.Proof} {numVars : ℕ}
  {constraints : Std.HashMap Lean.Omega.Coeffs Lean.Elab.Tactic.Omega.Fact} {equalities : Std.HashSet Lean.Omega.Coeffs}
  {eliminations : List (Lean.Elab.Tactic.Omega.Fact × ℕ × ℤ)} {possible : Bool}
  {proveFalse? : Option Lean.Elab.Tactic.Omega.Proof}
  {proveFalse?_spec :
    autoParam ((possible || proveFalse?.isSome) = true) Lean.Elab.Tactic.Omega.Problem.proveFalse?_spec._autoParam}
  {explanation? : Thunk String} {assumptions_1 : Array Lean.Elab.Tactic.Omega.Proof} {numVars_1 : ℕ}
  {constraints_1 : Std.HashMap Lean.Omega.Coeffs Lean.Elab.Tactic.Omega.Fact}
  {equalities_1 : Std.HashSet Lean.Omega.Coeffs} {eliminations_1 : List (Lean.Elab.Tactic.Omega.Fact × ℕ × ℤ)}
  {possible_1 : Bool} {proveFalse?_1 : Option Lean.Elab.Tactic.Omega.Proof}
  {proveFalse?_spec_1 :
    autoParam ((possible_1 || proveFalse?_1.isSome) = true) Lean.Elab.Tactic.Omega.Problem.proveFalse?_spec._autoParam}
  {explanation?_1 : Thunk String},
  { assumptions := assumptions, numVars := numVars, constraints := constraints, equalities := equalities,
        eliminations := eliminations, possible := possible, proveFalse? := proveFalse?,
        proveFalse?_spec := proveFalse?_spec, explanation? := explanation? } =
      { assumptions := assumptions_1, numVars := numVars_1, constraints := constraints_1, equalities := equalities_1,
        eliminations := eliminations_1, possible := possible_1, proveFalse? := proveFalse?_1,
        proveFalse?_spec := proveFalse?_spec_1, explanation? := explanation?_1 } →
    assumptions = assumptions_1 ∧
      numVars = numVars_1 ∧
        constraints = constraints_1 ∧
          equalities = equalities_1 ∧
            eliminations = eliminations_1 ∧
              possible = possible_1 ∧ proveFalse? = proveFalse?_1 ∧ explanation? = explanation?_1