exact match Classical.em p, Classical.em q with
| Or.inl pp,  _          => False.elim (h (Or.inl pp))
| Or.inr _,   Or.inl pq  => False.elim (h (Or.inr pq))
| Or.inr npp, Or.inr npq => And.intro npp npq
p q : Prop
h : ¬(p ∨ q)
⊢ ¬p ∧ ¬q
no goals