hid Show Code edit
##
## (-> (-> ph ph) [ ps)
## [ ps
##
thm (hid () (1 (-> (-> ph ph) ps)) ps
ph id 1 ax-mp)
ps
edit