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