∀ (motive : Lean.Meta.Grind.SolverTerms × Lean.Meta.Grind.PendingSolverPropagationsData✝ → Sort u_1)
  (s : Lean.Meta.Grind.SolverTerms) (p : Lean.Meta.Grind.PendingSolverPropagationsData✝)
  (h_1 : (s : Lean.Meta.Grind.SolverTerms) → (p : Lean.Meta.Grind.PendingSolverPropagationsData✝) → motive (s, p)),
  (match (s, p) with
    | (s, p) => h_1 s p) =
    h_1 s p