intros norm_x div_x
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x : A
⊢ (∀ (x_1 : A), ¬R x x_1) → normalizes R x
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x : A
norm_x : ∀ (x_1 : A), ¬R x x_1
div_x : diverge_from R x
⊢ False