no goals
L : Language
T : Theory L
α : Type w
M : Type w'
inst✝² : Structure L M
inst✝¹ : Nonempty M
inst✝ : M ⊨ T
v : α → M
φ : Formula L α
⊢ ↑Formula.equivSentence φ ∈ typeOf T v ↔ Formula.Realize φ v
simp