cases f_in
case intro.intro.intro.intro.refine_2
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
f : Formula
f_in : f ∈ Fs ∨ f ∈ Gs
⊢ evaluate M v f
case intro.intro.intro.intro.refine_2.inl
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
f : Formula
h✝ : f ∈ Fs
⊢ evaluate M v f

case intro.intro.intro.intro.refine_2.inr
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
f : Formula
h✝ : f ∈ Gs
⊢ evaluate M v f