simp [hq]
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
q : SyntacticFormula L
hq : q ∈ Δ
hhq : (Evalfm M ε) q
⊢ q ∈ (∃' p) :: Δ
no goals