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