Theorem: SetTheory.interpret_iff (SetTheory/Formula.lean)

State before:
V : Type u_1
inst✝ : SetTheory V
α✝ : Type
a✝ : Nat
p q : BoundedFormula α✝ a✝
v : α✝ → V
l : Fin a✝ → V
⊢ Interpret V (BoundedFormula.iff p q) v l ↔ (Interpret V p v l ↔ Interpret V q v l)
Tactic:
unfold BoundedFormula.iff
State after:
V : Type u_1
inst✝ : SetTheory V
α✝ : Type
a✝ : Nat
p q : BoundedFormula α✝ a✝
v : α✝ → V
l : Fin a✝ → V
⊢ Interpret V (BoundedFormula.and (BoundedFormula.imp p q) (BoundedFormula.imp q p)) v l ↔
    (Interpret V p v l ↔ Interpret V q v l)

State before:
V : Type u_1
inst✝ : SetTheory V
α✝ : Type
a✝ : Nat
p q : BoundedFormula α✝ a✝
v : α✝ → V
l : Fin a✝ → V
⊢ Interpret V (BoundedFormula.and (BoundedFormula.imp p q) (BoundedFormula.imp q p)) v l ↔
    (Interpret V p v l ↔ Interpret V q v l)
Tactic:
aesop
State after:
no goals