Progress with PEG-correctness proof.

- Reorient equality in inductive hypothesis to make rewriting work better
- Prove more cases (only 43 to go (!))