∀ {α : Type u_1} (motive : Option (Stream'.Seq1 (Option α)) → Sort u_2) (s' : Stream'.Seq (Option α))
  (h_1 : Unit → motive none) (h_2 : (s' : Stream'.Seq (Option α)) → motive (some (none, s')))
  (h_3 : (a : α) → (s' : Stream'.Seq (Option α)) → motive (some (some a, s'))),
  (match some (none, s') with
    | none => h_1 ()
    | some (none, s') => h_2 s'
    | some (some a, s') => h_3 a s') =
    h_2 s'