induction p using rec' <;>
simp [*, Semiterm.val_lMap, lMap_rel, lMap_nrel, eval_rel, eval_nrel]
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
no goals