{P : Sort u} →
  {solverId : ℕ} →
    {e : Lean.Expr} →
      {rest : Lean.Meta.Grind.SolverTerms} →
        {solverId' : ℕ} →
          {e' : Lean.Expr} →
            {rest' : Lean.Meta.Grind.SolverTerms} →
              Lean.Meta.Grind.SolverTerms.next solverId e rest = Lean.Meta.Grind.SolverTerms.next solverId' e' rest' →
                (solverId = solverId' → e = e' → rest = rest' → P) → P