a small look at another cheat

but not proved - the statement likely needs more assumptions.  also,
partial fix fo the last commit (which also introduced additional
assumptions). I think the build is still broken possibly due to the
extra automatic rewrite I added (or maybe it was broken before?), but
I'm getting on a plane now so can't fix.