explicit message for failed autoquickcheck

tyabbr/syntax/consts: replaced obsolete read_typ by Syntax.parse_typ/certify_typ;

avoid obsolete Sign.read_prop;

tuned proofs -- avoid implicit prems;

fixed imports path;

tuned proofs -- avoid open cases;

function package: using the names of the equations as case names turned out to be impractical => disabled

avoid name clashes when generating code for union, inter

oops -- avoid vacous goal message; tuned messages;

tuned messages; tuned;

avoid "import" as identifier, which is a keyword in Alice;

tuned presentation;