∀ (w : Lean.Meta.Grind.Order.NodeId) (k : Lean.Meta.Grind.Order.Weight) (proof : Lean.Expr)
  (w_1 : Lean.Meta.Grind.Order.NodeId) (k_1 : Lean.Meta.Grind.Order.Weight) (proof_1 : Lean.Expr),
  ({ w := w, k := k, proof := proof } = { w := w_1, k := k_1, proof := proof_1 }) =
    (w = w_1 ∧ k = k_1 ∧ proof = proof_1)