nic-justneg Show Code edit
# Show equivalence between negation and the Nicod version. To derive
# [[nic-dfneg]], apply [[nic-justbi]].
thm (nic-justneg () () (<-> (-. ps) (-/\ ps ps)) ps ps df-nand ps anidm notbii bitr2i)
(<-> (-. ps) (-/\ ps ps))
edit