constructor <;> apply refl_trans_clos.step <;> try constructor
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
confl : confluent R
x y z : A
red_x_y : R x y
red_x_z : R x z
⊢ refl_trans_clos R x y ∧ refl_trans_clos R x z
case a.left.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
confl : confluent R
x y z : A
red_x_y : R x y
red_x_z : R x z
⊢ R x y

case a.right.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
confl : confluent R
x y z : A
red_x_y : R x y
red_x_z : R x z
⊢ R x z