induction t <;> simp[*, Semiterm.lMap_func, Semiterm.val_func]
μ : 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
t : Semiterm L₁ μ n
⊢ Semiterm.val (extendStructure Φ s₁) e ε (Semiterm.lMap Φ t) = Semiterm.val s₁ e ε t
case func
μ : 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
arity✝ : ℕ
a✝¹ : L₁.Func arity✝
a✝ : Fin arity✝ → Semiterm L₁ μ n
a_ih✝ :
  ∀ (a : Fin arity✝), Semiterm.val (extendStructure Φ s₁) e ε (Semiterm.lMap Φ (a✝ a)) = Semiterm.val s₁ e ε (a✝ a)
⊢ (func (Φ.func a✝¹) fun i => Semiterm.val s₁ e ε (a✝ i)) = func a✝¹ fun i => Semiterm.val s₁ e ε (a✝ i)