pass auto-proved exhaustiveness properties to tactic;
rightly use "%_. False" instead of undefined for unspecified conditions;
get rid of ugly "if True then ... else Code.abort" in auto-generated code equations;
#special components for internal testing onlyvampire-1.0yices-1.0.28