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

State before:
V : Type u_1
inst✝ : SetTheory V
α✝ : Type
a✝ : Nat
p : BoundedFormula α✝ (a✝ + 1)
v : α✝ → V
l : Fin a✝ → V
⊢ Interpret V (BoundedFormula.exists p) v l ↔ ∃ x, Interpret V p v (Fin.snoc l x)
Tactic:
unfold BoundedFormula.exists
State after:
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)

State before:
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)
Tactic:
aesop
State after:
no goals