∀ (shortDeclName declName : Lean.Name) (levelNames : List Lean.Name) (binderIds : Array Lean.Syntax) (numParams : ℕ)
  (type : Lean.Expr) (shortDeclName_1 declName_1 : Lean.Name) (levelNames_1 : List Lean.Name)
  (binderIds_1 : Array Lean.Syntax) (numParams_1 : ℕ) (type_1 : Lean.Expr),
  ({ shortDeclName := shortDeclName, declName := declName, levelNames := levelNames, binderIds := binderIds,
        numParams := numParams, type := type } =
      { shortDeclName := shortDeclName_1, declName := declName_1, levelNames := levelNames_1, binderIds := binderIds_1,
        numParams := numParams_1, type := type_1 }) =
    (shortDeclName = shortDeclName_1 ∧
      declName = declName_1 ∧
        levelNames = levelNames_1 ∧ binderIds = binderIds_1 ∧ numParams = numParams_1 ∧ type = type_1)