Add triple notation for generalized post-condition

This changeset defines notation for the Iris style of writing Hoare triples:

{{{ P }}} e {{{ v1 .. vn; T, Q }}} := P ★ (∀ v1 .. vn, Q → Φ T) ⊢ WP e {{ Φ }}

For no good reason the notation is parsing only, although I do not declare it as such. We might want to do that though, since it might be too hard to understand a Hoare triple goal without unfolding it.

I have changed the barrier specifications to use the new notation in an attempt to demonstrate their usefulness (or, at a minimum, their applicability). The changes are rather minimal, as you can see.

Changes

First and foremost, the specifications change. (Duh!) Then, there are three kinds of changes to the proofs:

1. The first iIntros needs to take care of introducing Φ. No big deal, in my opinion.

2. Introducing the spatial assumptions needs one additional level of structure since we go from

   P1 ★ P2 ★ (∀ v, Q v -★ Φ v) to (P1 ★ P2) ★ (∀ v, Q v -★ Φ v)

3. A post-condition of True leads to the rather annoying hypothesis True -★ Φ v, which (as far as I can tell) cannot be made to behave the same as just (Φ v) in the context of iFrame.

Applicability

I have also looked at most other examples of specifications in heap_lang/lib. The notation seems to be applicable to almost all of them. The only place where I spotted an obvious mismatch is par.v, where the current lemmas have a later before the generalized post-condition, as in ... ★ (∀ .., ... -★ ▷ Φ ..) ⊢ WP ... We could always add another pair of notations for this special case, I suppose.

Nomenclature

I think "Texan triple" would be a good name, seeing how everything is bigger in Texas, including the number of curly braces.