constructor
case neg
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x✝ x : A
h✝ : ∀ (y : A), R x y → ∃ y_1, refl_trans_clos R y y_1 ∧ normal R y_1
h : ¬∃ y, R x y
⊢ refl_trans_clos R x x ∧ normal R x
case neg.left
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x✝ x : A
h✝ : ∀ (y : A), R x y → ∃ y_1, refl_trans_clos R y y_1 ∧ normal R y_1
h : ¬∃ y, R x y
⊢ refl_trans_clos R x x

case neg.right
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x✝ x : A
h✝ : ∀ (y : A), R x y → ∃ y_1, refl_trans_clos R y y_1 ∧ normal R y_1
h : ¬∃ y, R x y
⊢ normal R x