feat: print first goal after safe prefix in terminal mode

[semorrison]

When in terminal mode, print the (first) goal after the terminal prefix as part of the error message, so we get an indication of what progress aesop made, and where it got stuck.

Too often I write a structure where some auto_param field is not successfully filled in by aesop, and it's presumably just because a @[simp] lemma is missing. But to see the goal (and hence deduce the missing simp lemma), I have to add field := by aesop. I think with this change we'll just be able to see what we need immediately.

[JLimperg]

Ideas for improvements from our Zulip conversation:

• Remove the "initial goal" part of the error message since it's usually not useful.
• Collapse this part by default. (Needs core API changes; currently only trace nodes can be collapsed.)
• Make an option to remove this part, off by default.