∀ {name : Lean.Name} {levelParams : List Lean.Name} {type : Lean.Expr} {name_1 : Lean.Name}
  {levelParams_1 : List Lean.Name} {type_1 : Lean.Expr},
  { name := name, levelParams := levelParams, type := type } =
      { name := name_1, levelParams := levelParams_1, type := type_1 } →
    name = name_1 ∧ levelParams = levelParams_1 ∧ type = type_1