Prove completeness for common left-recursive parsing pattern.
Prove a better version of peg_linfix_complete and use it successfully.
Delete implausible (commented out) proof attempt on completeness.

The other approach is still looking plausible.
Modify the grammar to make completeness proof easier.

I've introduced a redundant non-terminal so that my linfix-lemma
applies to the TyVarList rule.
Extract my common tactics/theorems into a "parsing preamble" module.
Split soundness and completeness proofs into two script files.