Modify PEG to make completeness proof more likely.

It’s now a closer match to the shape of the CFG.

Also (commented out), some work towards a completeness result based on
showing that if the PEG fails, there is no parse tree. This together
with totality for the peg_eval relation would give what we need.
Progress with a completeness proof.