cases' joins with z h
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y : A
joins : _root_.joins R x y
⊢ _root_.joins R y x
case intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : A
h : refl_trans_clos R x z ∧ refl_trans_clos R y z
⊢ joins R y x