Theorem: refl_sym_is_sym_refl (Traat/chapter1.lean)

State before:
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))
Tactic:
apply both_inclusions <;> intros x y hyp <;> aesop
State after:
no goals