apply (reds_joins_left _) <;> trivial
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x z y : A
red_x_y : refl_trans_clos R x z
joins_y_z : joins R y z
joins_z_y : joins R z y
⊢ joins R x y
no goals