have eq_y_w : y = w := by apply normal_red <;> trivial
case intro.intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
conf : confluent R
x y z : A
red_x_y : refl_trans_clos R x y
red_x_z : refl_trans_clos R x z
norm_y : normal R y
norm_z : normal R z
wdg_y_z : wedge R y z
w : A
left✝ : refl_trans_clos R y w
right✝ : refl_trans_clos R z w
⊢ y = z
case intro.intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
conf : confluent R
x y z : A
red_x_y : refl_trans_clos R x y
red_x_z : refl_trans_clos R x z
norm_y : normal R y
norm_z : normal R z
wdg_y_z : wedge R y z
w : A
left✝ : refl_trans_clos R y w
right✝ : refl_trans_clos R z w
eq_y_w : y = w
⊢ y = z