{motive : Lean.Elab.Tactic.Omega.Problem → Sort u} →
  (t : Lean.Elab.Tactic.Omega.Problem) →
    ((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 : (possible || proveFalse?.isSome) = true) →
                      (explanation? : Thunk String) →
                        motive
                          { assumptions := assumptions, numVars := numVars, constraints := constraints,
                            equalities := equalities, eliminations := eliminations, possible := possible,
                            proveFalse? := proveFalse?, proveFalse?_spec := proveFalse?_spec,
                            explanation? := explanation? }) →
      motive t