have : (s.struc.lMap Φ).toStruc ⊧ σ :=
  h ⟨fun _ hq => Semiformula.models_lMap.mp <| hM.realize (Set.mem_image_of_mem _ hq)⟩
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
L₁ L₂ : Language
Φ : L₁ →ᵥ L₂
T : Theory L₁
σ : Sentence L₁
h : T ⊨[Struc L₁] σ
s : Struc L₂
hM : s ∈ Semantics.models (Struc L₂) (Theory.lMap Φ T)
⊢ s ⊧ (Semiformula.lMap Φ) σ
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
L₁ L₂ : Language
Φ : L₁ →ᵥ L₂
T : Theory L₁
σ : Sentence L₁
h : T ⊨[Struc L₁] σ
s : Struc L₂
hM : s ∈ Semantics.models (Struc L₂) (Theory.lMap Φ T)
this : (Structure.lMap Φ s.struc).toStruc ⊧ σ
⊢ s ⊧ (Semiformula.lMap Φ) σ