match Classical.em p, Classical.em q with
| Or.inl hp, Or.inl hq  => exact False.elim (h (And.intro hp hq))
| _,         Or.inr hnq => exact Or.inr hnq
| Or.inr hnp, _        => exact Or.inl hnp
p q : Prop
h : ¬(p ∧ q)
⊢ ¬p ∨ ¬q
no goals