Theorem: LO.FirstOrder.models_iff (Logic/FirstOrder/Basic/Semantics/Semantics.lean)

State before:
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type u_1
inst✝ : Nonempty M
s : Structure L M
T U : Theory L
σ : Sentence L
⊢ M ⊧ₘ σ ↔ (Semiformula.Evalf s Empty.elim) σ
Tactic:
simp [models_def]
State after:
no goals