exact match Classical.em P, Classical.em Q with
| Or.inr np, _ => Or.inl np
| _, Or.inr nq => Or.inr nq
| Or.inl p, Or.inl q =>
  absurd (propext (Iff.intro (λ _ => q) (λ _ => p))) h
P Q : Prop
h : ¬P = Q
⊢ ¬P ∨ ¬Q
no goals