Change my-hint-raw.lsp back to the version of proving (equal 2 3)