pm2.07 Show Code edit
## Disjunction is Idempotent
thm (pm2.07 () () (-> ph (\/ ph ph))
ph ph olc
(-> ph (\/ ph ph))
)
edit