intros x red_norm div
case a
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
⊢ ∀ (x : A), (∀ (y : A), R x y → normalizes R y) → normalizes R x
case a
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✝ x : A
red_norm : ∀ (y : A), R x y → normalizes R y
div : diverge_from R x
⊢ False