DEFINITION not_abbr_abst()
TYPE =
       not (eq B Abbr Abst)
BODY =
Show proof