Some progress with PEG -> CFG proof

Up to showing that the PEG’s handling of left-associative infixes is
correct. I hope one lemma will blow all the many cases of this pattern
away.