rcases claim with ⟨⟨Gs,γ⟩, Gsγ_in, claim⟩
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
Fs : List Formula
Fδ_in : (Fs, ε) ∈ H α
w_Con : evaluate M w (Con (Yset (Fs, ε) (⌈β⌉ψ)))
claim : ∃ Gγ ∈ H β, evaluate M w (Con (Yset Gγ ψ))
⊢ ∃ Fδ ∈ H (α;'β), evaluate M w (Con (Yset Fδ ψ))
case intro.mk.intro
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
Fs : List Formula
Fδ_in : (Fs, ε) ∈ H α
w_Con : evaluate M w (Con (Yset (Fs, ε) (⌈β⌉ψ)))
Gs : List Formula
γ : List Program
Gsγ_in : (Gs, γ) ∈ H β
claim : evaluate M w (Con (Yset (Gs, γ) ψ))
⊢ ∃ Fδ ∈ H (α;'β), evaluate M w (Con (Yset Fδ ψ))