simp [lMap_rel, lMap_nrel, *]
case hex
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✝ : ℕ
p✝ : Semiformula L₁ ξ (n✝ + 1)
a✝ : ((lMap Φ) p✝).fvarList = p✝.fvarList
⊢ ((lMap Φ) (∃' p✝)).fvarList = (∃' p✝).fvarList
no goals