apply npa
case a.h
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
npa : ¬P a
p : ∀ (x : A), ¬P x → ¬R a x
⊢ False
case a.h
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
npa : ¬P a
p : ∀ (x : A), ¬P x → ¬R a x
⊢ P a