apply semi_confluent_implies_confluent
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
conf' : confluent' R
⊢ confluent R
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
conf' : confluent' R
⊢ semi_confluent R