∀ {α : Type u_1} (motive : Computation α → Prop) (x : Computation α),
  (∀ (val : Stream' (Option α)) (property : ∀ ⦃n : ℕ⦄ ⦃a : α⦄, val n = some a → val (n + 1) = some a),
      motive ⟨val, property⟩) →
    motive x