olc Show Code edit
## Introduction of a disjunct
thm (olc () () (-> ph (\/ ps ph))
ph (-. ps) ax-1
(-> ph (-> (-. ps) ph))
orrd
(-> ph (\/ ps ph))
)
edit