match Classical.em p, Classical.em q with
| _,         Or.inl hq  => exact Or.inr (Or.inr hq)
| Or.inl hp, Or.inr hnq => apply Or.inl
                           intro f
                           exact absurd (f hp) hnq
| Or.inr hnp, _         => exact Or.inr (Or.inl hnp)
p q : Prop
⊢ ¬(p → q) ∨ ¬p ∨ q
no goals