intros str_conf
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
⊢ strongly_confluent R → confluent R
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
str_conf : strongly_confluent R
⊢ confluent R