intros joins
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y : A
⊢ joins R x y → joins R y x
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y : A
joins : _root_.joins R x y
⊢ _root_.joins R y x