exists φ x
case intro
M : Type u_2
N : Type u_1
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
s : Structure L M
φ : M ≃ N
x✝ : ℕ
e : Fin x✝ → N
ε : μ → N
p : Semiformula L μ (x✝ + 1)
x : M
h : (Eval s (x :> ⇑φ.symm ∘ e) (⇑φ.symm ∘ ε)) p
⊢ ∃ x, (Eval (ofEquiv φ) (x :> e) ε) p
case intro
M : Type u_2
N : Type u_1
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
s : Structure L M
φ : M ≃ N
x✝ : ℕ
e : Fin x✝ → N
ε : μ → N
p : Semiformula L μ (x✝ + 1)
x : M
h : (Eval s (x :> ⇑φ.symm ∘ e) (⇑φ.symm ∘ ε)) p
⊢ (Eval (ofEquiv φ) (φ x :> e) ε) p