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