casesi Show Code edit
## Proof by cases
thm (casesi () (1 (-> ph ps) 2 (-> (-. ph) ps)) ps
2 1 ph ps cases ax-mp ax-mp)
ps
edit