have wdg_y_z : wedge _ y z := Exists.intro x ⟨ red_x_y, red_x_z ⟩
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
⊢ y = z
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
⊢ y = z