unfold semi_confluent
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
sc : diamond R
⊢ semi_confluent R
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
sc : diamond R
⊢ ∀ (x y z : A), R x y → refl_trans_clos R x z → joins R y z