rcases Gγ_in_l with ⟨l, ⟨⟨aaa, bbb, ⟨_in_Hβ,def_l⟩ ⟩, Fsδ_in_l⟩ ⟩
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
Fs : List Formula
δ : List Program
w_Con : evaluate M w (Con (Yset (Fs, δ) ψ))
Gs : List Formula
Gγ_in : (Gs, ε) ∈ H α
Gγ_in_l : ∃ l, (∃ a b, (a, b) ∈ H β ∧ [(Gs ∪ a, b)] = l) ∧ (Fs, δ) ∈ l
⊢ ∃ Fδ ∈ H α, evaluate M w (Con (Yset Fδ (⌈β⌉ψ)))
case intro.intro.intro.intro.intro
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
Fs : List Formula
δ : List Program
w_Con : evaluate M w (Con (Yset (Fs, δ) ψ))
Gs : List Formula
Gγ_in : (Gs, ε) ∈ H α
l : List (List Formula × List Program)
Fsδ_in_l : (Fs, δ) ∈ l
aaa : List Formula
bbb : List Program
_in_Hβ : (aaa, bbb) ∈ H β
def_l : [(Gs ∪ aaa, bbb)] = l
⊢ ∃ Fδ ∈ H α, evaluate M w (Con (Yset Fδ (⌈β⌉ψ)))