case a.step a b c red_a_b _red_b_c ih =>
  intros d red_a_d
  have h := (sc _ _ _ red_a_b red_a_d)
  cases' h with e h
  cases' h with red_b_e red_d_e
  apply red_joins <;> aesop
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
no goals