∀ {motive : Batteries.RBColor → Sort u} (t : Batteries.RBColor) (red : motive Batteries.RBColor.red)
  («else» : Nat.hasNotBit 1 t.ctorIdx → motive t) (h : Nat.hasNotBit 1 t.ctorIdx),
  Batteries.RBNode.balance1._sparseCasesOn_2 t red «else» = «else» h