revert h z y
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm_R : normalizing R
weak : weakly_confluent R
y z x : A
h : refl_trans_clos R x y ∧ refl_trans_clos R x z
⊢ joins R y z
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm_R : normalizing R
weak : weakly_confluent R
x : A
⊢ ∀ (y z : A), refl_trans_clos R x y ∧ refl_trans_clos R x z → joins R y z