∀ {α : Type u} {motive : Option α → Sort u_1} (t : Option α) (none : motive none)
  («else» : Nat.hasNotBit 1 t.ctorIdx → motive t) (h : Nat.hasNotBit 1 t.ctorIdx),
  Stream'.WSeq.LiftRelO._sparseCasesOn_1 t none «else» = «else» h