intros tr_x_y
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : A
⊢ trans_clos R x y → trans_clos R y z → trans_clos R x z
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : A
tr_x_y : trans_clos R x y
⊢ trans_clos R y z → trans_clos R x z