intros ih x
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
⊢ (∀ (P : A → Prop), (∀ (x : A), (∀ (y : A), R x y → P y) → P x) → ∀ (x : A), P x) → normalizing R
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
ih : ∀ (P : A → Prop), (∀ (x : A), (∀ (y : A), R x y → P y) → P x) → ∀ (x : A), P x
x : A
⊢ normalizes R x