trivial
case refl
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x : A
norm : normal R x
⊢ x = x

case step
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y : A
norm : normal R x
b✝ : A
a✝¹ : R x b✝
a✝ : refl_trans_clos R b✝ y
⊢ x = y
case step
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y : A
norm : normal R x
b✝ : A
a✝¹ : R x b✝
a✝ : refl_trans_clos R b✝ y
⊢ x = y