Allow `iSpecialize` to be nested.

This MR introduces the new specialization pattern (H spat1 .. spatn), which first recursively specializes the hypothesis H using the specialization patterns spat1 .. spatn.

A basic example:

H : P
H1 : P -∗ Q
H2 : Q -∗ R

Now you can do things like iSpecialize ("H2" with "(H1 H)").

In practice, I found this useful when dealing with wp_wand. In the heap-lang logical relations development in iris-examples I often have things like:

H : P -∗ WP e {{ Φ }}
H2: P
-------------
WP e {{ Ψ }}

where Φ and Ψ are not the same. Using the new specialization patterns, one can do things like iApply (wp_wand with "(H [//])").

Future work

There are many ways to further extend specialization patterns such as also allowing nested uses of iSpecialize in goal patterns and framing, e.g. [$(H1 H2) (H3 H4)]. I have not really seen a need for that, so I did not implement these things.