simp [Semiformula.models_lMap, Theory.lMap, modelsTheory_iff, @modelsTheory_iff (T := T₁)]
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
L₁ L₂ : Language
Φ : L₁ →ᵥ L₂
M : Type u
inst✝ : Nonempty M
s₂ : Structure L₂ M
T₁ : Theory L₁
⊢ M ⊧ₘ* lMap Φ T₁ ↔ M ⊧ₘ* T₁
no goals