notnot1 Show Code edit
## Double Negative
thm (notnot1 () () (-> ph (-. (-. ph)))
ph dnr)
(-> ph (-. (-. ph)))
edit