. aesop
case 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
⊢ confluent fun x y => (fun x x_1 => refl_trans_clos (fun x y => S x y) x x_1) x y
no goals