simp_all [H]
case intro.intro.intro.intro.refine_1
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
Fs : List Formula
u_Fs : ∀ f ∈ Fs, evaluate M v f
Fδ_in : (Fs, ε) ∈ H α
v_α_u : relate M α v v
u_β_w : relate M β v w
Gs : List Formula
η : List Program
Gη_in : (Gs, η) ∈ H β
v_Gs : ∀ f ∈ Gs, evaluate M v f
v_η_w : relateSeq M η v w
⊢ (Fs ∪ Gs, η) ∈ H (α;'β)
case intro.intro.intro.intro.refine_1
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
Fs : List Formula
u_Fs : ∀ f ∈ Fs, evaluate M v f
Gs : List Formula
η : List Program
Fδ_in : (Fs, []) ∈ H α
v_α_u : relate M α v v
u_β_w : relate M β v w
Gη_in : (Gs, η) ∈ H β
v_Gs : ∀ f ∈ Gs, evaluate M v f
v_η_w : relateSeq M η v w
⊢ ∃ 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