simp
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
⊢ ((fun R R' => ∀ (x y : A), R x y → R' x y) (fun x x_1 => R x x_1) fun x x_1 => S x x_1) →
    ((fun R R' => ∀ (x y : A), R x y → R' x y) (fun x x_1 => S x x_1) fun x x_1 => refl_trans_clos R x x_1) →
      confluent S → confluent R
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
⊢ (∀ (x y : A), R x y → S x y) → (∀ (x y : A), S x y → refl_trans_clos R x y) → confluent S → confluent R