simp only [List.mem_join, List.mem_map, Prod.exists]
case h.left
ψ : 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, γ) ψ))
⊢ (Fs ∪ Gs, γ) ∈
    (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.left
ψ : 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, γ) ψ))
⊢ ∃ 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 ∪ Gs, γ) ∈ l