exact ⟨⟨M, i, s.extendStructure Φ⟩, by
  simp[Semantics.realizeSet_iff]
  intro σ hσ
  exact (Structure.extendStructure.models_lMap Φ injf injr s σ).mpr (hM.realize hσ)⟩
case intro.mk
L L₁ L₂ : Language
Φ : L₁ →ᵥ L₂
injf : ∀ (k : ℕ), Function.Injective Φ.func
injr : ∀ (k : ℕ), Function.Injective Φ.rel
T : Theory L₁
M : Type u
i : Nonempty M
s : Structure L₁ M
hM : { Dom := M, nonempty := i, struc := s } ⊧* T
⊢ Satisfiable (⇑(Semiformula.lMap Φ) '' T)
no goals