Theory for the negation operation ($\neg$). The negation of TRUE is FALSE. The negation of FALSE is TRUE. It is defined to only act on a Boolean such that $\neg A$ only evaluates to TRUE if $A$ is FALSE and only evaluates to FALSE if $A$ is TRUE.
TRUE
FALSE
import proveit %theory