cases γ
W✝ : Type
M : KripkeModel W✝
γ : Program
v w : W✝
v_γ_w : relate M γ v w
⊢ ∃ Fδ ∈ H γ, (M, v)⊨Fδ.1 ∧ relateSeq M Fδ.2 v w
case atom_prog
W✝ : Type
M : KripkeModel W✝
v w : W✝
a✝ : ℕ
v_γ_w : relate M (·a✝) v w
⊢ ∃ Fδ ∈ H (·a✝), (M, v)⊨Fδ.1 ∧ relateSeq M Fδ.2 v w

case sequence
W✝ : Type
M : KripkeModel W✝
v w : W✝
a✝¹ a✝ : Program
v_γ_w : relate M (a✝¹;'a✝) v w
⊢ ∃ Fδ ∈ H (a✝¹;'a✝), (M, v)⊨Fδ.1 ∧ relateSeq M Fδ.2 v w

case union
W✝ : Type
M : KripkeModel W✝
v w : W✝
a✝¹ a✝ : Program
v_γ_w : relate M (a✝¹⋓a✝) v w
⊢ ∃ Fδ ∈ H (a✝¹⋓a✝), (M, v)⊨Fδ.1 ∧ relateSeq M Fδ.2 v w

case star
W✝ : Type
M : KripkeModel W✝
v w : W✝
a✝ : Program
v_γ_w : relate M (∗a✝) v w
⊢ ∃ Fδ ∈ H (∗a✝), (M, v)⊨Fδ.1 ∧ relateSeq M Fδ.2 v w

case test
W✝ : Type
M : KripkeModel W✝
v w : W✝
a✝ : Formula
v_γ_w : relate M (?'a✝) v w
⊢ ∃ Fδ ∈ H (?'a✝), (M, v)⊨Fδ.1 ∧ relateSeq M Fδ.2 v w