intros x y z red_x_y h
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
⊢ ∀ (x y z : A), R x y → refl_trans_clos R y z → refl_trans_clos R x z
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : A
red_x_y : R x y
h : refl_trans_clos R y z
⊢ refl_trans_clos R x z