Generation of efficient validity test checks for ? terms.

If there’s an existential inside the theorem it’s not going to be
well-suited to evaluation with EVAL.
Prove that the PEG-parser always terminates when asked to parse a
REPLPhrase.

Here, “termination” means that peg_exec mmlPEG ... always returns a
Result value.