case func k f v ih =>
  exact extendStructure.func Φ s₁ (injf k) f (fun i => Semiterm.val s₁ e ε (v i))
μ : Type u_1
L L₁ L₂ : Language
Φ : L₁ →ᵥ L₂
injf✝ : ∀ (k : ℕ), Function.Injective Φ.func
injr : ∀ (k : ℕ), Function.Injective Φ.rel
M : Type u
inst✝ : Nonempty M
s₁✝ : Structure L₁ M
n : ℕ
e : Fin n → M
ε : μ → M
injf : ∀ (k : ℕ), Function.Injective Φ.func
s₁ : Structure L₁ M
k : ℕ
f : L₁.Func k
v : Fin k → Semiterm L₁ μ n
ih : ∀ (a : Fin k), Semiterm.val (extendStructure Φ s₁) e ε (Semiterm.lMap Φ (v a)) = Semiterm.val s₁ e ε (v a)
⊢ (func (Φ.func f) fun i => Semiterm.val s₁ e ε (v i)) = func f fun i => Semiterm.val s₁ e ε (v i)
no goals