aesop
case intro.intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : A
red_x_y : R x y
w : A
left✝ : refl_trans_clos R y w
right✝ : refl_trans_clos R z w
⊢ refl_trans_clos R x w ∧ refl_trans_clos R z w
no goals