{α : Type u_1} →
  (s : Computation α) →
    (motive : (v : Computation α) → s.destruct = Sum.inr v → Sort u_2) →
      (v : Computation α) →
        (H : s.destruct = Sum.inr v) →
          ((a : Stream' (Option α)) →
              (s' : ∀ ⦃n : ℕ⦄ ⦃a_1 : α⦄, a n = some a_1 → a (n + 1) = some a_1) →
                (H : s.destruct = Sum.inr ⟨a, s'⟩) → motive ⟨a, s'⟩ H) →
            motive v H