∀ (levelParams : Array Lean.Name) (type value : Lean.Expr) (levelArgs : Array Lean.Level) (exprArgs : Array Lean.Expr)
  (levelParams_1 : Array Lean.Name) (type_1 value_1 : Lean.Expr) (levelArgs_1 : Array Lean.Level)
  (exprArgs_1 : Array Lean.Expr),
  ({ levelParams := levelParams, type := type, value := value, levelArgs := levelArgs, exprArgs := exprArgs } =
      { levelParams := levelParams_1, type := type_1, value := value_1, levelArgs := levelArgs_1,
        exprArgs := exprArgs_1 }) =
    (levelParams = levelParams_1 ∧ type = type_1 ∧ value = value_1 ∧ levelArgs = levelArgs_1 ∧ exprArgs = exprArgs_1)