intros conf x y z red_x_y red_x_z norm_y norm_z
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
⊢ confluent R → ∀ (x y z : A), refl_trans_clos R x y → refl_trans_clos R x z → normal R y → 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
⊢ y = z