[vim-mode] add support for `Proof` modifiers

[hrutvik]

Handle things like Proof[exclude_simps thms] as follows:

• ha previously selected a goal-statement in between Theorem/Triviality and Proof. Now it also selects the Proof keyword and associated [...] (including over multiple lines).

• To help ha above, modify the HOLSelect function so that it opens any folds found at the endpoint of its selection.

• hG goal-setting command now invokes proofManagerLib.new_goalstack and BasicProvers.mk_tacmod as suggested by @mn200. It searches the selected "goal" for the Proof keyword to pass the correct bit to mk_tacmod. It remains compatible with selections which do not include the Proof keyword.

[mn200]

Discord chat suggests there is one further change required for this PR to get the vim mode able to apply tactics properly in an Proof-modified block. I will merge once that's also in place.

[mn200]

Awesome!