WIP: Prepend introduction pattern `H.ipat`.

The new introduction pattern H.ipat prepends the name H to all names appearing in ipat.

For example:

Lemma test_iDestruct_prepend_1 P Q :
  P ∗ Q -∗ Q ∗ P.
Proof. iIntros "H.[P Q]".

This will give hypotheses HP and HQ.

This feature will be particularly useful with the record-like syntax that @tchajed @jtassaro @jung and me are working on.

TODO

• Bikeshed about the syntax. The period . may cause annoyances with the electric terminator in Emacs?