olcd Show Code edit
## Introduction of a disjunct
thm (olcd () (hyp (-> ph ps)) (-> ph (\/ ch ps))
hyp
(-> ph ps)
ps ch olc
(-> ps (\/ ch ps))
syl
(-> ph (\/ ch ps))
)
edit