pm2.61i Show Code edit
## Proof by cases
##
## (-> ph [ ps)
## (-> (-. ph) [ ps)
## [ ps
##
thm (pm2.61i () (1 (-> ph ps) 2 (-> (-. ph) ps)) ps
1 2 casesi)
ps
edit