rfl
case succ
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✝ : ℕ
a✝ : ∀ (p : Semiformula L₁ ξ (n + n✝)), (lMap Φ) (∃^[n✝] p) = ∃^[n✝] (lMap Φ) p
p : Semiformula L₁ ξ (n + (n✝ + 1))
⊢ (lMap Φ) p = (lMap Φ) p
no goals