. intros a npa
  apply Classical.byContradiction
  simp; intros p
  apply npa
  apply IH; intros y ry
  apply Classical.byContradiction; intros npy
  apply (p y npy ry)
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
P : A → Prop
IH : ∀ (x : A), (∀ (y : A), R x y → P y) → P x
x : A
norm : normalizes R x
h : ¬P x
⊢ ∀ (a : A), ¬P a → ∃ b, ¬P b ∧ R a b
no goals