id1 Show Code edit
## Identity
##
## This version is proved directly from the axioms for demonstration purposes.
## This proof is a popular example in the literature. For an alternative proof
## see id.
##
##
## (-> ph ph)
##
thm (id1 () () (-> ph ph)
ph ps ax-1 ph (-> ps ph) ax-1 ph (-> ps ph) ph ax-2 ax-mp ax-mp)
(-> ph ph)
edit