∀ {view : Lean.Elab.Command.InductiveView} {levelNames : List Lean.Name} {numParams : ℕ} {type : Lean.Expr}
  {origParams : Array Lean.Expr} {view_1 : Lean.Elab.Command.InductiveView} {levelNames_1 : List Lean.Name}
  {numParams_1 : ℕ} {type_1 : Lean.Expr} {origParams_1 : Array Lean.Expr},
  { view := view, levelNames := levelNames, numParams := numParams, type := type, origParams := origParams } =
      { view := view_1, levelNames := levelNames_1, numParams := numParams_1, type := type_1,
        origParams := origParams_1 } →
    view = view_1 ∧ levelNames = levelNames_1 ∧ numParams = numParams_1 ∧ type = type_1 ∧ origParams = origParams_1