aesop
V : Type u_1
inst✝ : SetTheory V
α✝ : Type
a✝ : Nat
p : BoundedFormula α✝ (a✝ + 1)
v : α✝ → V
l : Fin a✝ → V
⊢ Interpret V (BoundedFormula.not (BoundedFormula.all (BoundedFormula.not p))) v l ↔ ∃ x, Interpret V p v (Fin.snoc l x)
no goals