constructor
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, δ ++ [β]) ∈
      (List.map
          (fun x =>
            match x with
            | (F, δ) =>
              if δ = ε then
                (List.map
                    (fun x =>
                      match x with
                      | (G, δ') => [(F ∪ G, δ')])
                    (H β)).join
              else [(F, δ ++ [β])])
          (H α)).join ∧
    evaluate M w (Con (Yset (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_ε : ¬δ = ε
⊢ (Fs, δ ++ [β]) ∈
    (List.map
        (fun x =>
          match x with
          | (F, δ) =>
            if δ = ε then
              (List.map
                  (fun x =>
                    match x with
                    | (G, δ') => [(F ∪ G, δ')])
                  (H β)).join
            else [(F, δ ++ [β])])
        (H α)).join

case h.right
ψ : 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_ε : ¬δ = ε
⊢ evaluate M w (Con (Yset (Fs, δ ++ [β]) ψ))