fix more proofs broken by case-expressions on string literals

I think the issue was in what Define generated for the function
definitions... I haven't touched them, just fixed these proofs.
Hopefully this won't cause more problems later, but if so then maybe
using a different Pmatch heuristic is necessary when making the
definitions.