Change recursive domain to `proto = 1 + (action * (V → proto → PROP))`.

By moving the later further to the outside, we can kill many occurences of Next, and get rid of laters/except_0s at awkward positions. Also we can have a sensible eliminator proto_elim.