I've learned a lot about maximizing laziness and its
relation to getting shit to compute on open terms over
these last few days. I believe this lesson will remain relevant
for many years to come.
Also, deleted zipper because I'm pretty sure it can't be made
lazy even in principle, and therefore it is useless.
It's much more general and less ad-hoc.
On the other hand, I have no idea how it works (or if it works).
I derived it pretty much by just writing out the type and putting
in whatever I hoped would make the typechecker happy.
I came up with that particular type signature by working on
the new linear derivations, which require much more sophisticated
types of substitution than I originally accounted for. I believe
substs will be sufficiently general (if it works!!).