Support `old(..)` in quantifier triggers
Currently Prusti supports Expr::{Local, Const, FuncApp, DomainFuncApp} in quantifier triggers:
https://github.com/viperproject/prusti-dev/blob/0f079017d1fb75f0264b1e652746f16266a25773/prusti-viper/src/encoder/mir/pure/specifications/encoder_poly.rs#L303-L311
Should these also be supported when wrapped in old(..), i.e. Expr::LabelledOld? Down at the Prusti level, there are some cases where this is hard-coded, but currently it is not possible for end-users to write a similar specification:
https://github.com/viperproject/prusti-dev/blob/0f079017d1fb75f0264b1e652746f16266a25773/prusti-viper/src/encoder/procedure_encoder.rs#L5118-L5123
For example, such user specifications maybe be needed when extern_specing <[T]>::copy_within.