L : Language
L' : Language
M : Type w
N : Type ?u.69331
P : Type ?u.69334
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
n l : ℕ
φ ψ : BoundedFormula L α l
θ : BoundedFormula L α (Nat.succ l)
v : α → M
xs : Fin l → M
⊢ (∃ x, ¬Realize (∼θ) v (snoc xs x)) ↔ ∃ a, Realize θ v (snoc xs a)
L : Language
L' : Language
M : Type w
N : Type ?u.69331
P : Type ?u.69334
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
n l : ℕ
φ ψ : BoundedFormula L α l
θ : BoundedFormula L α (Nat.succ l)
v : α → M
xs : Fin l → M
⊢ Realize (∃'θ) v xs ↔ ∃ a, Realize θ v (snoc xs a)
rw [BoundedFormula.ex, realize_not, realize_all, not_forall]
no goals
L : Language
L' : Language
M : Type w
N : Type ?u.69331
P : Type ?u.69334
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
n l : ℕ
φ ψ : BoundedFormula L α l
θ : BoundedFormula L α (Nat.succ l)
v : α → M
xs : Fin l → M
⊢ (∃ x, ¬Realize (∼θ) v (snoc xs x)) ↔ ∃ a, Realize θ v (snoc xs a)
simp_rw [realize_not, Classical.not_not]