Theorem: LO.FirstOrder.Structure.eval_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 : ℕ
p : Semiformula L₂ μ n
e : Fin n → M
ε : μ → M
⊢ (Semiformula.Eval (add L₁ L₂ M) e ε) ((Semiformula.lMap (Language.Hom.add₂ L₁ L₂)) p) ↔ (Semiformula.Eval str₂ e ε) p
Tactic:
induction p using Semiformula.rec' <;>
  simp [*, Language.Hom.rel_add₂, Semiformula.eval_rel,
    Semiformula.lMap_rel, Semiformula.eval_nrel, Semiformula.lMap_nrel]
State after:
no goals