have : Evalfm M ε p ∨ ∃ r ∈ Δ, Evalfm M ε r := by simpa using sound dp M ε
L : Language
Δ : List (SyntacticFormula L)
p q : SyntacticFormula L
dp : Derivation (p :: Δ)
dq : Derivation (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
dp : Derivation (p :: Δ)
dq : Derivation (q :: Δ)
M : Type u_1
s : Structure L M
ε : ℕ → M
this : (Evalfm M ε) p ∨ ∃ r ∈ Δ, (Evalfm M ε) r
⊢ ∃ p_1 ∈ p ⋏ q :: Δ, (Evalfm M ε) p_1