∀ (inductiveVal : Lean.InductiveVal) (nminors : ℕ) (majorDecl : Lean.LocalDecl) (majorTypeFn : Lean.Expr)
  (majorTypeArgs majorTypeIndices : Array Lean.Expr) (inductiveVal_1 : Lean.InductiveVal) (nminors_1 : ℕ)
  (majorDecl_1 : Lean.LocalDecl) (majorTypeFn_1 : Lean.Expr) (majorTypeArgs_1 majorTypeIndices_1 : Array Lean.Expr),
  ({ inductiveVal := inductiveVal, nminors := nminors, majorDecl := majorDecl, majorTypeFn := majorTypeFn,
        majorTypeArgs := majorTypeArgs, majorTypeIndices := majorTypeIndices } =
      { inductiveVal := inductiveVal_1, nminors := nminors_1, majorDecl := majorDecl_1, majorTypeFn := majorTypeFn_1,
        majorTypeArgs := majorTypeArgs_1, majorTypeIndices := majorTypeIndices_1 }) =
    (inductiveVal = inductiveVal_1 ∧
      nminors = nminors_1 ∧
        majorDecl = majorDecl_1 ∧
          majorTypeFn = majorTypeFn_1 ∧ majorTypeArgs = majorTypeArgs_1 ∧ majorTypeIndices = majorTypeIndices_1)