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;
#additional components to be bundled for releaseProofGeneral-4.2