simp
case a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
a✝² : ∀ (x y : A), R x y → S x y
a✝¹ : ∀ (x y : A), S x y → refl_trans_clos R x y
a✝ : confluent S
⊢ ∀ (x y : A), (fun x x_1 => R x x_1) x y → (fun x x_1 => ?a.S✝ x x_1) x y

case a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
a✝² : ∀ (x y : A), R x y → S x y
a✝¹ : ∀ (x y : A), S x y → refl_trans_clos R x y
a✝ : confluent S
⊢ ∀ (x y : A), (fun x x_1 => ?a.S✝ x x_1) x y → (fun x x_1 => refl_trans_clos R x x_1) x y

case a.S
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
a✝² : ∀ (x y : A), R x y → S x y
a✝¹ : ∀ (x y : A), S x y → refl_trans_clos R x y
a✝ : confluent S
⊢ A → A → Prop
case a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
a✝² : ∀ (x y : A), R x y → S x y
a✝¹ : ∀ (x y : A), S x y → refl_trans_clos R x y
a✝ : confluent S
⊢ ∀ (x y : A), R x y → ?a.S✝ x y

case a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
a✝² : ∀ (x y : A), R x y → S x y
a✝¹ : ∀ (x y : A), S x y → refl_trans_clos R x y
a✝ : confluent S
⊢ ∀ (x y : A), (fun x x_1 => ?a.S✝ x x_1) x y → (fun x x_1 => refl_trans_clos R x x_1) x y

case a.S
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
a✝² : ∀ (x y : A), R x y → S x y
a✝¹ : ∀ (x y : A), S x y → refl_trans_clos R x y
a✝ : confluent S
⊢ A → A → Prop