DEFINITION not()
TYPE =
       Prop→Prop
BODY =
Show proof