So there's two different ways to implement `Stream`s: strict hd and lazy tl or lazy hd and tl. I originally had the former and I just switched to the latter.

For strict `hd`, the best constructor would be `cons : a -> (() -> (Stream a)) -> Stream a`
```Haskell
fibs = S.cons 0 <| \() ->
         S.cons 1 <| \() ->
           S.zipWith (+) fibs (tl fibs))
```
For lazy `hd`, the best non-record ctor would probably be `make : (() -> (a, Stream a)) -> Stream a` (alternative name: `fromThunk`)
```Haskell
fibs = S.make <| \() ->
         ( 0
         , S.make <| \() ->
           ( 1
           , S.zipWith (+) fibs (tl fibs)))
```
The alternative non-record ctor for lazy hd would be `make : (() -> a) -> (() -> (Stream a)) -> Stream a` but I think this would be worse to use since it would require more thunk construction. 

There's also the current ctor `make : (() -> { hd : a, tl : Stream a }) -> Stream a` which I actually like the most API-wise. It makes it very clear that you're defining the hd and tl of your `Stream` by "punning" `.hd` and `.tl` with `hd` and `tl` here in a way that IMO is very readable. Also as a general idea I think codata should be defined by destructors (`hd` and `tl`) instead of constructors (`cons`). You should think of a `Stream` as something that is defined as a `hd` and a `tl`, instead of an sequence of `cons`es (which is of course actually impossible to have). Does that make sense? I just think we should make the difference between data and codata pretty explicit because the other approach (define codata just like data) is one of my least favorite things about Haskell/Coq.

I think it makes sense to have a lazy `hd` though since it IS a lazy data structure so you would expect that none of its values are evaluated until they are requested. This is the way it would be evaluated in a lazy language like Haskell so I think we should do it that way to give people the ultimate laziness.