Improve and test more proof mode error messages

• Print hypothesis name without [INamed].
• Take some local recursive helper functions out to be bound via Local Ltac instead.
• Fix some bugs (errors because none of the arms of a match worked) along the way.

Unfortunately I was not sure how to trigger all of these codepaths, so it is possible that I also changed some where the H already is a string.

@robbertkrebbers If you could provide some testcases that trigger error conditions that are not covered yet, that'd be great.

Fixes #201 (closed)