Theorem: sym_inv (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) ((fun R x y => R y x) R) (sym_clos R)
Tactic:
aesop
State after:
no goals