the meta `model_projection` has the following form ``` meta "model_projection" function f ``` where `f` is a unary function say from some type `t`. It allows to obtain values in counterexamples say when `t` is an abstract type. It can also be used when `t` is not abstract. Yet, when `t` is an alias type then the current implementation produces some unexpected behavior, and indeed it is unclear what should be done in such a case. It is thus preferable that Why3 simply signals an error when `t` is an alias type.