prove the other cheat in compilerProofsScript.sml introduced by tup+eq