Description
It's not immediately obvious to a new user how to get a completed proof once you have one.
Currently you need to "unify" all, then select the checkmark on qed. That's not obvious, and that action should be obvious.
Perhaps next to "unify" could be a "Generate compressed proof" button. It would try to unify all the statements (if that hasn't already been done), and then if qed can be proved, do the equivalent of selecting the checkmark next to qed. That would make it obvious, and also it's easier to select.
Also, perhaps when a proof of "qed" is first completely proved (back to all leaves), there can be a statement like "Congratulations, you've proved the conclusion. Select 'Generate compressed proof' or the checkmark next to the qed statement". That would make it more discoverable, and as well as being a delightful message to see.