prove remaining (uncommented) cheats in initialProgramScript.sml