dfor2-lemma Show Code edit
## Alternative Definition of OR Lemma
thm (dfor2-lemma () () (<-> (-> (-. ph) ps) (-> (-> ph ps) ps))
ph ps pm2.6
(-> (-> (-. ph) ps) (-> (-> ph ps) ps))
ph ps pm2.21
(-> (-. ph) (-> ph ps))
ps imim1i
(-> (-> (-> ph ps) ps) (-> (-. ph) ps))
impbii
(<-> (-> (-. ph) ps) (-> (-> ph ps) ps))
)
edit