intros d red_a_d
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
⊢ ∀ (y : A), R a y → joins R y c
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
⊢ joins R d c