pm2.43b Show Code edit
## Absorb redundant antecedent
thm (pm2.43b () (1 (-> ps (-> ph (-> ps ch)))) (-> ph (-> ps ch))
1 pm2.43a com12)
(-> ph (-> ps ch))
edit