use Fs, δ
case h.left
ψ : 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, δ) (⌈β⌉ψ)))
δ_not_ε : ¬δ = ε
⊢ ∃ a b,
    (a, b) ∈ H α ∧
      (if b = [] then (List.map (fun x => [(a ∪ x.1, x.2)]) (H β)).join else [(a, b ++ [β])]) = [(Fs, δ ++ [β])]
case h
ψ : 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, δ) (⌈β⌉ψ)))
δ_not_ε : ¬δ = ε
⊢ (Fs, δ) ∈ H α ∧
    (if δ = [] then (List.map (fun x => [(Fs ∪ x.1, x.2)]) (H β)).join else [(Fs, δ ++ [β])]) = [(Fs, δ ++ [β])]