Allow multiple hidden hints

[TentativeConvert]

It would occassionaly be nice to be able to offer incremental hidden hints, e.g. just a rough hint the first time the user asks for more help, and a second more detailed hint if the user still asks for help. I tried to do this with two consecutive hidden hints, but the current behaviour seems to be that these both get shown at the same time (I guess because they are associated with the same proof state.)