olci Show Code edit
## Introduction of a disjunct
thm (olci () (hyp ph) (\/ ps ph)
hyp
ph
ph ps olc
(-> ph (\/ ps ph))
ax-mp
(\/ ps ph)
)
edit