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

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