induction p using Semiformula.rec' <;> try simp [lMap_rel, lMap_nrel, *]
L✝ : Language
ξ✝ : Type u_1
n n₁ n₂✝ n₂ m m₁ m₂ m₃ : ℕ
L : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_2
Φ✝ Φ : L₁ →ᵥ L₂
p : Semiformula L₁ ξ n
⊢ ((lMap Φ) p).fvarList = p.fvarList
case hrel
L✝ : Language
ξ✝ : Type u_1
n n₁ n₂✝ n₂ m m₁ m₂ m₃ : ℕ
L : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_2
Φ✝ Φ : L₁ →ᵥ L₂
n✝ k✝ : ℕ
r✝ : L₁.Rel k✝
v✝ : Fin k✝ → Semiterm L₁ ξ n✝
⊢ (rel (Φ.rel r✝) fun i => Semiterm.lMap Φ (v✝ i)).fvarList = (rel r✝ v✝).fvarList

case hnrel
L✝ : Language
ξ✝ : Type u_1
n n₁ n₂✝ n₂ m m₁ m₂ m₃ : ℕ
L : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_2
Φ✝ Φ : L₁ →ᵥ L₂
n✝ k✝ : ℕ
r✝ : L₁.Rel k✝
v✝ : Fin k✝ → Semiterm L₁ ξ n✝
⊢ (nrel (Φ.rel r✝) fun i => Semiterm.lMap Φ (v✝ i)).fvarList = (nrel r✝ v✝).fvarList