Progress with the PEG correctness/soundness lemma (7 subgoals to go)