have norm_trans := normalizes_trans _ norm_R
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
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm_R : normalizing R
weak : weakly_confluent R
x : A
norm_trans : normalizing fun x x_1 => trans_clos R x x_1
⊢ ∀ (y z : A), refl_trans_clos R x y ∧ refl_trans_clos R x z → joins R y z