biid Show Code edit
## Identity
thm (biid () () (<-> ph ph)
ph id
(-> ph ph)
ph id
(-> ph ph)
impbii)
(<-> ph ph)
edit