have : Evalfm M ε p ∨ Evalfm M ε q ∨ ∃ q ∈ Δ, Evalfm M ε q := by simpa using sound d M ε
L : Language
Δ : List (SyntacticFormula L)
p q : SyntacticFormula L
d : Derivation (p :: q :: Δ)
M : Type u_1
s : Structure L M
ε : ℕ → M
⊢ ∃ p_1 ∈ p ⋎ q :: Δ, (Evalfm M ε) p_1
L : Language
Δ : List (SyntacticFormula L)
p q : SyntacticFormula L
d : Derivation (p :: q :: Δ)
M : Type u_1
s : Structure L M
ε : ℕ → M
this : (Evalfm M ε) p ∨ (Evalfm M ε) q ∨ ∃ q ∈ Δ, (Evalfm M ε) q
⊢ ∃ p_1 ∈ p ⋎ q :: Δ, (Evalfm M ε) p_1