cases' h with w h
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
h : joins RX X.a X.d
⊢ False
case intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
w : X
h : refl_trans_clos RX X.a w ∧ refl_trans_clos RX X.d w
⊢ False