cases' h with e h
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
sc : diamond R
x z a b c : A
red_a_b : R a b
_red_b_c : refl_trans_clos R b c
ih : ∀ (y : A), R b y → joins R y c
d : A
red_a_d : R a d
h : ∃ w, R b w ∧ R d w
⊢ joins R d c
case intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
sc : diamond R
x z a b c : A
red_a_b : R a b
_red_b_c : refl_trans_clos R b c
ih : ∀ (y : A), R b y → joins R y c
d : A
red_a_d : R a d
e : A
h : R b e ∧ R d e
⊢ joins R d c