exp32 Show Code edit
## Export Inference
thm (exp32 () (exp32.1 (-> (/\ ph (/\ ps ch)) th)) (-> ph (-> ps (-> ch th))) exp32.1 ex exp3a)
(-> ph (-> ps (-> ch th)))
edit