induction h
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
sc : diamond R
x z : A
h : refl_trans_clos R x z
⊢ ∀ (y : A), R x y → joins R y z
case a.refl
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
sc : diamond R
x z a✝ : A
⊢ ∀ (y : A), R a✝ y → joins R y a✝

case a.step
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
sc : diamond R
x z a✝² b✝ c✝ : A
a✝¹ : R a✝² b✝
a✝ : refl_trans_clos R b✝ c✝
a_ih✝ : ∀ (y : A), R b✝ y → joins R y c✝
⊢ ∀ (y : A), R a✝² y → joins R y c✝