∀ {premises : Array (Option Lean.Expr)} {levels : Array (Option Lean.Level)} {premises_1 : Array (Option Lean.Expr)}
  {levels_1 : Array (Option Lean.Level)},
  { premises := premises, levels := levels } = { premises := premises_1, levels := levels_1 } →
    premises = premises_1 ∧ levels = levels_1