cases em (δ = ε)
case intro.intro.intro.intro.intro.intro
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
u : W✝
v_α_u : relate M α v u
u_β_w : relate M β u w
Fs : List Formula
δ : List Program
Fδ_in : (Fs, δ) ∈ H α
u_Fs : ∀ f ∈ Fs, evaluate M v f
v_δ_u : relateSeq M δ v u
⊢ ∃ Fδ ∈ H (α;'β), (M, v)⊨Fδ.1 ∧ relateSeq M Fδ.2 v w
case intro.intro.intro.intro.intro.intro.inl
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
u : W✝
v_α_u : relate M α v u
u_β_w : relate M β u w
Fs : List Formula
δ : List Program
Fδ_in : (Fs, δ) ∈ H α
u_Fs : ∀ f ∈ Fs, evaluate M v f
v_δ_u : relateSeq M δ v u
h✝ : δ = ε
⊢ ∃ Fδ ∈ H (α;'β), (M, v)⊨Fδ.1 ∧ relateSeq M Fδ.2 v w

case intro.intro.intro.intro.intro.intro.inr
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
u : W✝
v_α_u : relate M α v u
u_β_w : relate M β u w
Fs : List Formula
δ : List Program
Fδ_in : (Fs, δ) ∈ H α
u_Fs : ∀ f ∈ Fs, evaluate M v f
v_δ_u : relateSeq M δ v u
h✝ : ¬δ = ε
⊢ ∃ Fδ ∈ H (α;'β), (M, v)⊨Fδ.1 ∧ relateSeq M Fδ.2 v w