disambiguated grammar

tuned proofs

tuned

simplified 'typedef' specifications: discontinued implicit set definition and alternative name;

discontinued typedef with alternative name;

discontinued obsolete typedef (open) syntax;

discontinued typedef with implicit set_def;

merged

increading indexes to avoid clashes in the set_comprehension_pointfree simproc

no special treatment of errors inside goal forks without transaction id, to avoid duplication in plain build with sequential log, for example;