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