intros norm_R weak
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
⊢ normalizing R → weakly_confluent R → confluent R
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm_R : normalizing R
weak : weakly_confluent R
⊢ confluent R