{stream : Type u} →
  {value : Type v} →
    {motive : Std.Stream stream value → Sort u_1} →
      (t : Std.Stream stream value) →
        ((next? : stream → Option (value × stream)) → motive { next? := next? }) → motive t