intros x y wedge
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
⊢ (fun R R' => ∀ (x y : A), R x y → R' x y) (wedge R) fun x x_1 => refl_trans_sym_clos R x x_1
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y : A
wedge : _root_.wedge R x y
⊢ refl_trans_sym_clos R x y