rcases s with ⟨⟨M, i, s⟩, hM⟩
L L₁ L₂ : Language
Φ : L₁ →ᵥ L₂
injf : ∀ (k : ℕ), Function.Injective Φ.func
injr : ∀ (k : ℕ), Function.Injective Φ.rel
T : Theory L₁
s : Satisfiable T
⊢ Satisfiable (⇑(Semiformula.lMap Φ) '' T)
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)