Theorem: Smt.Reconstruct.Prop.notEquivElim2 (Smt/Reconstruct/Prop/Lemmas.lean)

State before:
⊢ ∀ {P Q : Prop}, ¬P = Q → ¬P ∨ ¬Q
Tactic:
intros P Q h
State after:
P Q : Prop
h : ¬P = Q
⊢ ¬P ∨ ¬Q

State before:
P Q : Prop
h : ¬P = Q
⊢ ¬P ∨ ¬Q
Tactic:
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
State after:
no goals