apply both_inclusions <;> intros x y hyp <;> aesop
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
⊢ (fun R R' => ∀ (x y : A), R x y ↔ R' x y) (refl_clos (sym_clos R)) (sym_clos (refl_clos R))
no goals