bi2 Show Code edit
## Infer Right to Left
## right('Infer', '←')
thm (bi2 () () (-> (<-> ph ps) (-> ps ph))
ph ps def-bi-1 and2d)
(-> (<-> ph ps) (-> ps ph))
edit