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