DEFINITION not_void_abst()
TYPE =
       not (eq B Void Abst)
BODY =
Show proof