Theorem: both_inclusions (Traat/chapter1.lean)

State before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
R' : A → A → Prop
⊢ (fun R R' => ∀ (x y : A), R x y → R' x y) R R' →
    (fun R R' => ∀ (x y : A), R x y → R' x y) R' R → (fun R R' => ∀ (x y : A), R x y ↔ R' x y) R R'
Tactic:
aesop
State after:
no goals