himp1 Show Code edit
##
## (-> (-> (-> ph ps) ch) (-> ps ch))
##
thm (himp1 () () (-> (-> (-> ph ps) ch) (-> ps ch))
ps ph ax-1 ch imim1i)
(-> (-> (-> ph ps) ch) (-> ps ch))
edit