have : ∃ p ∈ Δ, Evalfm M ε p := sound d M ε
L : Language
Γ Δ : Sequent L
d : Derivation Δ
ss : Δ ⊆ Γ
M : Type u_1
s : Structure L M
ε : ℕ → M
⊢ ∃ p ∈ Γ, (Evalfm M ε) p
L : Language
Γ Δ : Sequent L
d : Derivation Δ
ss : Δ ⊆ Γ
M : Type u_1
s : Structure L M
ε : ℕ → M
this : ∃ p ∈ Δ, (Evalfm M ε) p
⊢ ∃ p ∈ Γ, (Evalfm M ε) p