apply h
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
commut_r_s : commute R S
conf_r : confluent R
conf_s : confluent S
h :
  (fun R R' => ∀ (x y : A), R x y → R' x y) ((fun R S x y => R x y ∨ S x y) R S)
    ((fun R S x y => ∃ z, R x z ∧ S z y) (fun x x_1 => refl_trans_clos R x x_1) fun x x_1 => refl_trans_clos S x x_1)
⊢ ∀ (x y : A), (fun x x_1 => (fun R S x y => R x y ∨ S x y) R S x x_1) x y → (fun x x_1 => ?S x x_1) x y
no goals