apply IH
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
norm : normalizing R
x : A
⊢ ∀ (x : A), (∀ (y : A), ?R x y → P y) → P x
no goals