logically atomic triples: add private postcondition

This is needed for examples!59.

The notation looks like this:

<<{ ∀∀ x, atomic_pre x }>> code @ ∅ <<{ ∃∃ y, atomic_post x y | z, RET val; private_post x y z }>>

To make this consistent with the triples without private postcondition, their notation changes as follows:

<<{ ∀∀ x, atomic_pre x }>> code @ ∅ <<{ ∃∃ y, atomic_post x y | z, RET val }>>

This also better reflects that the return value doesn't "happen" with the linearization point. However, it is a breaking change.

Fixes #473 (closed) by changing the parentheses.