Exhaustivity checks lets non exhaustive case fail later
When running why3 prove -L . modulo.mlw
there is a non exhaustivity error during VC generation. It as not been detected during typing of q.mlw
. --debug no_vc_eval
could be needed otherwise the error appears somewhere else.