pm2.1 Show Code edit
# Theorem *2.1 of [bib/WhiteheadRussell] p. 101.
## Law of excluded middle
thm (pm2.1 () () (\/ (-. ph) ph) ph notnot2 orri)
(\/ (-. ph) ph)
edit