expcom Show Code edit
## Export & Commute
thm (expcom () (exp.1 (-> (/\ ph ps) ch)) (-> ps (-> ph ch)) exp.1 ex com12)
(-> ps (-> ph ch))
edit