Make proof failures really fail in pc-verification.
Save/export my superior induction principle for graphOf
Notes for my own benefit about how pcg_eval is defined.
Checking in some work in progress.