∀ {motive : Lean.Level → Sort u} (t : Lean.Level) (zero : motive Lean.Level.zero)
  (max : (a a_1 : Lean.Level) → motive (a.max a_1)) (succ : (a : Lean.Level) → motive a.succ)
  («else» : Nat.hasNotBit 7 t.ctorIdx → motive t) (h : Nat.hasNotBit 7 t.ctorIdx),
  Lean.Level.geq.go._sparseCasesOn_1✝ t zero max succ «else» = «else» h