using `model_projection` on alias types should be forbidden

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.