apply norm
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y✝ : A
norm : normal R x
y : A
a✝¹ : R x y
a✝ : refl_trans_clos R y y✝
x✝ : ¬x = y✝
⊢ False
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y✝ : A
norm : normal R x
y : A
a✝¹ : R x y
a✝ : refl_trans_clos R y y✝
x✝ : ¬x = y✝
⊢ ∃ x', R x x'