Use Hint more strategically
As noted by @mlesourd (!32 (comment 38961)), using Hint
s could make some of our proofs easier / shorter by automating away tedious steps. Going forward, we should introduce Hint
s in Prosa and come up with some guidelines for when it's a good idea to do so.