id Show Code edit
## Identity
##
## (-> ph ph)
##
##
## See id1 for an alternative proof directly from the axioms.
##
thm (id () () (-> ph ph)
ph ps ax-1 ph (-> ps ph) ax-1 mpd)
(-> ph ph)
edit