Add the notion of a `DeepThunk` and generation for this

[Equilibris]

When it comes to expressing co-recursive functions, a state type is required to seed the progress. This state often also stores at what point the expression is in. This can be for a corec function on streams that repeats each element once more can have a state of a boolean and the stream that flips the boolean every other emission. This behaviour can be a bit funny to encode correctly in general corec functions so we use DeepThunk (the trace) to construct it instead. Generation of these objects takes a bit of work as seen in Ind.lean but the general categorical object resides in DeepThunk.lean.

Additionally, to this we split some files out and move some code around. This might be worth doing in a separate PR though.

[alexkeizer]

See comments on the other PR, they also apply here