Support quantifiers inside pure functions

[mueller55]

When pure functions are used to abbreviate recurring assertions (e.g. invariants that are conjoined to many pre- and postconditions), it would be useful if one could write (pure) assertions, in particular, quantifiers in their bodies.

There are various alternative designs (e.g., using postconditions of abstract functions, using macros), but those have subtle implications for triggering. So we need to explore what the best option is. We might even have to change Viper to avoid matching loops.

[Aurel300]

This should be covered by #390.