orc Show Code edit
## Introduction of a disjunct
thm (orc () () (-> ph (\/ ph ps))
ph ps pm2.24
(-> ph (-> (-. ph) ps))
orrd
(-> ph (\/ ph ps))
)
edit