intros x y z red_x_y red_x_z
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
str_conf : strongly_confluent R
⊢ ∀ (x y z : A), R x y → refl_trans_clos R x z → joins R y z
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
str_conf : strongly_confluent R
x y z : A
red_x_y : R x y
red_x_z : refl_trans_clos R x z
⊢ joins R y z