simp [models_iff, ←eval_translation_iff, Matrix.empty_eq]
L L' : Language
inst✝³ : L.Eq
T : Theory L
ι : Interpretation T L'
M : Type u
inst✝² : Nonempty M
s : Structure L M
inst✝¹ : Structure.Eq L M
inst✝ : M ⊧ₘ* T
σ : Sentence L'
⊢ M ⊧ₘ ι.translation σ ↔ ι.Sub M ⊧ₘ σ
no goals