Code suggestions

[ejgallego]

In order to try the repair code feature, we can suggest users two hints for Qed / Admitted proofs:

• when the proof is broken, suggest the user to use Admitted.
• when a proof that is not broken ends in Admitted, suggest switching it to Qed.

Whether having Admitted upstream is a good thing, I don't know.

[ejgallego]

This is more a showcase for the LSP feature than a useful thing, as our error recovery will insert admitted on Qed , so I dunno.

[ejgallego]

Another interesting one is to suggest the user to add proof terminators to proofs that are closed by a tactic.