induction p using Semiformula.rec' <;> simp[*, val_lMap Φ e ε injf s₁, Semiformula.lMap_rel, Semiformula.lMap_nrel, eval_rel, eval_nrel]
μ : Type u_1
L L₁ L₂ : Language
Φ : L₁ →ᵥ L₂
injf : ∀ (k : ℕ), Function.Injective Φ.func
injr : ∀ (k : ℕ), Function.Injective Φ.rel
M : Type u
inst✝ : Nonempty M
s₁ : Structure L₁ M
n : ℕ
e : Fin n → M
ε : μ → M
p : Semiformula L₁ μ n
⊢ (Eval (extendStructure Φ s₁) e ε) ((lMap Φ) p) ↔ (Eval s₁ e ε) p
case hrel
μ : Type u_1
L L₁ L₂ : Language
Φ : L₁ →ᵥ L₂
injf : ∀ (k : ℕ), Function.Injective Φ.func
injr : ∀ (k : ℕ), Function.Injective Φ.rel
M : Type u
inst✝ : Nonempty M
s₁ : Structure L₁ M
n : ℕ
ε : μ → M
n✝ k✝ : ℕ
r✝ : L₁.Rel k✝
v✝ : Fin k✝ → Semiterm L₁ μ n✝
e : Fin n✝ → M
⊢ (rel (Φ.rel r✝) fun i => Semiterm.val s₁ e ε (v✝ i)) ↔ rel r✝ fun i => Semiterm.val s₁ e ε (v✝ i)

case hnrel
μ : Type u_1
L L₁ L₂ : Language
Φ : L₁ →ᵥ L₂
injf : ∀ (k : ℕ), Function.Injective Φ.func
injr : ∀ (k : ℕ), Function.Injective Φ.rel
M : Type u
inst✝ : Nonempty M
s₁ : Structure L₁ M
n : ℕ
ε : μ → M
n✝ k✝ : ℕ
r✝ : L₁.Rel k✝
v✝ : Fin k✝ → Semiterm L₁ μ n✝
e : Fin n✝ → M
⊢ (¬rel (Φ.rel r✝) fun i => Semiterm.val s₁ e ε (v✝ i)) ↔ ¬rel r✝ fun i => Semiterm.val s₁ e ε (v✝ i)