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.

changed title from Change rec domain eq to proto = 1 + (action * ▶ (V → proto → PROP)). to Change recursive domain to proto = 1 + (action * ▶ (V → proto → PROP)).

changed the description

added 2 commits

• c801fc33 - 1 commit from branch master
• 51a90f82 - Change rec domain eq to `proto = 1 + (action * (V → proto → PROP))`.

Compare with previous version

This looks like a good change for the mechanisation, but it leaves the model a bit weirder to explain, in regards to why the value and proposition are under laters, if its not -really- necessary.

LGTM but discuss the above at some point.

mentioned in commit d0342a67

merged