Theorem: LO.FirstOrder.Structure.val_lMap_sigma (Logic/FirstOrder/Basic/Model.lean)

State before:
ι : Type u_4
L : ι → Language
M : Type u_1
str : (i : ι) → Structure (L i) M
i : ι
μ : Type u_2
n : ℕ
t : Semiterm (L i) μ n
e : Fin n → M
ε : μ → M
⊢ Semiterm.val (sigma L M) e ε (Semiterm.lMap (Language.Hom.sigma L i) t) = Semiterm.val (str i) e ε t
Tactic:
induction t <;> simp [Semiterm.val, Language.Hom.func_sigma, *]
State after:
no goals