Try to get the compiler proof working with cheats

No success.  Theorem statements need to change to accomodate the new
type of Con, Conv, and Pcon, and it isn't obvious to me what's the best
way.