simp
L : Language
Δ : List (SyntacticFormula L)
p : Semiformula L ℕ (Nat.succ 0)
t : Semiterm L ℕ 0
d : Derivation ([→ t].hom p :: Δ)
M : Type u_1
s : Structure L M
ε : ℕ → M
hp : (Evalm M ![Semiterm.valm M ![] ε t] ε) p
⊢ ∃' p ∈ (∃' p) :: Δ
no goals