Wed Aug 19 15:41:37 EDT 2015

curried Comp function induction

The induction steps are

(t -> m t)      ->  (t -> t -> m t)
(t -> t -> m t) ->  (t -> t -> t -> m t)

where the t can be different but are kept same here for clarity.

problem is that we can't generate any variables outside of the monad.

There doesn't seem to be a generic way around this apart from lifting:
m t -> m t -> m t

It's also not that important...