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