∀ (motive : Lean.Meta.Grind.SolverTerms → Lean.Meta.Grind.SolverTerms → Sort u_1) (id₁ : ℕ) (lhs : Lean.Expr)
  (lhsTerms : Lean.Meta.Grind.SolverTerms) (id₂ : ℕ) (rhs : Lean.Expr) (rhsTerms : Lean.Meta.Grind.SolverTerms)
  (h_1 : (x : Lean.Meta.Grind.SolverTerms) → motive Lean.Meta.Grind.SolverTerms.nil x)
  (h_2 : (x : Lean.Meta.Grind.SolverTerms) → motive x Lean.Meta.Grind.SolverTerms.nil)
  (h_3 :
    (id₁ : ℕ) →
      (lhs : Lean.Expr) →
        (lhsTerms : Lean.Meta.Grind.SolverTerms) →
          (id₂ : ℕ) →
            (rhs : Lean.Expr) →
              (rhsTerms : Lean.Meta.Grind.SolverTerms) →
                motive (Lean.Meta.Grind.SolverTerms.next id₁ lhs lhsTerms)
                  (Lean.Meta.Grind.SolverTerms.next id₂ rhs rhsTerms)),
  (match Lean.Meta.Grind.SolverTerms.next id₁ lhs lhsTerms, Lean.Meta.Grind.SolverTerms.next id₂ rhs rhsTerms with
    | Lean.Meta.Grind.SolverTerms.nil, x => h_1 x
    | x, Lean.Meta.Grind.SolverTerms.nil => h_2 x
    | Lean.Meta.Grind.SolverTerms.next id₁ lhs lhsTerms, Lean.Meta.Grind.SolverTerms.next id₂ rhs rhsTerms =>
      h_3 id₁ lhs lhsTerms id₂ rhs rhsTerms) =
    h_3 id₁ lhs lhsTerms id₂ rhs rhsTerms