use ((H β).map (fun ⟨Gs',δ'⟩ => [⟨Fs ∪ Gs', δ'⟩])).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
case h
ψ : 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, γ) ψ))
⊢ (∃ a b,
      (a, b) ∈ H α ∧
        (if b = ε then (List.map (fun x => [(a ∪ x.1, x.2)]) (H β)).join else [(a, b ++ [β])]) =
          (List.map
              (fun x =>
                match x with
                | (Gs', δ') => [(Fs ∪ Gs', δ')])
              (H β)).join) ∧
    (Fs ∪ Gs, γ) ∈
      (List.map
          (fun x =>
            match x with
            | (Gs', δ') => [(Fs ∪ Gs', δ')])
          (H β)).join