revert red_x_z x
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x z y : A
red_x_z : R x z
red_z_y : refl_trans_clos R z y
⊢ trans_clos R x y
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
z y : A
red_z_y : refl_trans_clos R z y
⊢ ∀ {x : A}, R x z → trans_clos R x y