Otherwise, we would accept (mpv <- ghost v; let x = mpv in ...)
where both x and mpv are non-ghost.

(does not make much sense without polymorphism)

Coq realization for int.Power (mostly to keep Coq proofs that were in power.mlw)

prover shortcuts: the shortcuts information can be in the prover section in order to reduce the number of section in why3.conf