Theorem: LO.FirstOrder.Semiformula.eval_lMap (Logic/FirstOrder/Basic/Semantics/Semantics.lean)

State before:
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
L₁ : Language
L₂ : Language
Φ : L₁ →ᵥ L₂
M : Type u
inst✝ : Nonempty M
s₂ : Structure L₂ M
n : ℕ
e : Fin n → M
ε : μ → M
p : Semiformula L₁ μ n
⊢ (Eval s₂ e ε) ((lMap Φ) p) ↔ (Eval (Structure.lMap Φ s₂) e ε) p
Tactic:
induction p using rec' <;>
simp [*, Semiterm.val_lMap, lMap_rel, lMap_nrel, eval_rel, eval_nrel]
State after:
no goals