constructor <;> apply refl_trans_clos_transitive <;> trivial
case intro.intro.intro.intro.intro.intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
confl : confluent R
x✝ y✝ x y z : A
red_x_y : refl_trans_sym_clos R x y
red_y_z : refl_trans_sym_clos R y z
w1 : A
h11 : refl_trans_clos R x w1
h12 : refl_trans_clos R y w1
w2 : A
h21 : refl_trans_clos R y w2
h22 : refl_trans_clos R z w2
h' : wedge R w1 w2
w : A
h3 : refl_trans_clos R w1 w
h4 : refl_trans_clos R w2 w
⊢ refl_trans_clos R x w ∧ refl_trans_clos R z w
no goals