{α : Type u_1} →
  (motive : Option (Stream'.Seq1 α) → Option (Stream'.Seq1 α) → Sort u_2) →
    (x x_1 : Option (Stream'.Seq1 α)) →
      (Unit → motive none none) →
        ((a : α) → (s : Stream'.Seq α) → (a' : α) → (s' : Stream'.Seq α) → motive (some (a, s)) (some (a', s'))) →
          ((x x_2 : Option (Stream'.Seq1 α)) →
              (x = none → x_2 = none → False) →
                (∀ (a : α) (s : Stream'.Seq α) (a' : α) (s' : Stream'.Seq α),
                    x = some (a, s) → x_2 = some (a', s') → False) →
                  motive x x_2) →
            motive x x_1