∀ (optionsPerPos : Lean.PrettyPrinter.Delaborator.OptionsPerPos) (currNamespace : Lean.Name)
  (openDecls : List Lean.OpenDecl) (inPattern : Bool) (subExpr : Lean.SubExpr) (depth : ℕ)
  (optionsPerPos_1 : Lean.PrettyPrinter.Delaborator.OptionsPerPos) (currNamespace_1 : Lean.Name)
  (openDecls_1 : List Lean.OpenDecl) (inPattern_1 : Bool) (subExpr_1 : Lean.SubExpr) (depth_1 : ℕ),
  ({ optionsPerPos := optionsPerPos, currNamespace := currNamespace, openDecls := openDecls, inPattern := inPattern,
        subExpr := subExpr, depth := depth } =
      { optionsPerPos := optionsPerPos_1, currNamespace := currNamespace_1, openDecls := openDecls_1,
        inPattern := inPattern_1, subExpr := subExpr_1, depth := depth_1 }) =
    (optionsPerPos = optionsPerPos_1 ∧
      currNamespace = currNamespace_1 ∧
        openDecls = openDecls_1 ∧ inPattern = inPattern_1 ∧ subExpr = subExpr_1 ∧ depth = depth_1)