simp [H] at Fδ_in
case mpr.intro.mk.intro
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
Fs : List Formula
δ : List Program
Fδ_in : (Fs, δ) ∈ H (α;'β)
w_Con : evaluate M w (Con (Yset (Fs, δ) ψ))
⊢ ∃ Fδ ∈ H α, evaluate M w (Con (Yset Fδ (⌈β⌉ψ)))
case mpr.intro.mk.intro
ψ : Formula
W : Type
M : KripkeModel W
w : W
α β : Program
Fs : List Formula
δ : List Program
w_Con : evaluate M w (Con (Yset (Fs, δ) ψ))
Fδ_in :
  ∃ l,
    (∃ a b,
        (a, b) ∈ H α ∧ (if b = [] then (List.map (fun x => [(a ∪ x.1, x.2)]) (H β)).join else [(a, b ++ [β])]) = l) ∧
      (Fs, δ) ∈ l
⊢ ∃ Fδ ∈ H α, evaluate M w (Con (Yset Fδ (⌈β⌉ψ)))