DEFINITION not_abbr_void()
TYPE =
       not (eq B Abbr Void)
BODY =
Show proof