apply semi_confluent_implies_confluent
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
sc : diamond R
⊢ confluent R
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
sc : diamond R
⊢ semi_confluent R