rcases this with (hp | hq | ⟨r, hr, hhr⟩)
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
case inl
L : Language
Δ : List (SyntacticFormula L)
p q : SyntacticFormula L
d : Derivation (p :: q :: Δ)
M : Type u_1
s : Structure L M
ε : ℕ → M
hp : (Evalfm M ε) p
⊢ ∃ p_1 ∈ p ⋎ q :: Δ, (Evalfm M ε) p_1

case inr.inl
L : Language
Δ : List (SyntacticFormula L)
p q : SyntacticFormula L
d : Derivation (p :: q :: Δ)
M : Type u_1
s : Structure L M
ε : ℕ → M
hq : (Evalfm M ε) q
⊢ ∃ p_1 ∈ p ⋎ q :: Δ, (Evalfm M ε) p_1

case inr.inr.intro.intro
L : Language
Δ : List (SyntacticFormula L)
p q : SyntacticFormula L
d : Derivation (p :: q :: Δ)
M : Type u_1
s : Structure L M
ε : ℕ → M
r : SyntacticFormula L
hr : r ∈ Δ
hhr : (Evalfm M ε) r
⊢ ∃ p_1 ∈ p ⋎ q :: Δ, (Evalfm M ε) p_1