aesop
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)
no goals