∀ {α : Type u} {motive : Option α → Sort u_1} (t : Option α) (some : (val : α) → motive (some val))
  («else» : Nat.hasNotBit 2 t.ctorIdx → motive t) (h : Nat.hasNotBit 2 t.ctorIdx),
  Lean.Elab.Tactic.Try.isAccessible._sparseCasesOn_1✝ t some «else» = «else» h