bi1 Show Code edit
## Infer Left to Right
## right('Infer', '→')
thm (bi1 () () (-> (<-> ph ps) (-> ph ps))
ph ps def-bi-1 and1d)
(-> (<-> ph ps) (-> ph ps))
edit