Robotswana 1: unfold stdBasisMatrix kills hints

[TentativeConvert]

I'm not sure why anyone would want to unfold stdBasisMatrix in this level, but it turns out students do this, and then they don’t get any hints. Not sure how to deal with this. We probably do not want to add an additional branch for every single potential unfold statement in every step of every proof.

[joneugster]

We once had a discussion about having hints which trigger up to definitional equality, which may solve thos problem bit inteoduce others. Let's talk aboit hints on Tuesday