cases γ
W✝ : Type
M : KripkeModel W✝
v w : W✝
γ : Program
v_γ_w : relate M γ v w
ℓ : TP γ
v_conF : (M, v)⊨Con (F γ ℓ)
⊢ ∃ δ ∈ P γ ℓ, relateSeq M δ v w
case atom_prog
W✝ : Type
M : KripkeModel W✝
v w : W✝
a✝ : ℕ
v_γ_w : relate M (·a✝) v w
ℓ : TP (·a✝)
v_conF : (M, v)⊨Con (F (·a✝) ℓ)
⊢ ∃ δ ∈ P (·a✝) ℓ, relateSeq M δ v w

case sequence
W✝ : Type
M : KripkeModel W✝
v w : W✝
a✝¹ a✝ : Program
v_γ_w : relate M (a✝¹;'a✝) v w
ℓ : TP (a✝¹;'a✝)
v_conF : (M, v)⊨Con (F (a✝¹;'a✝) ℓ)
⊢ ∃ δ ∈ P (a✝¹;'a✝) ℓ, relateSeq M δ v w

case union
W✝ : Type
M : KripkeModel W✝
v w : W✝
a✝¹ a✝ : Program
v_γ_w : relate M (a✝¹⋓a✝) v w
ℓ : TP (a✝¹⋓a✝)
v_conF : (M, v)⊨Con (F (a✝¹⋓a✝) ℓ)
⊢ ∃ δ ∈ P (a✝¹⋓a✝) ℓ, relateSeq M δ v w

case star
W✝ : Type
M : KripkeModel W✝
v w : W✝
a✝ : Program
v_γ_w : relate M (∗a✝) v w
ℓ : TP (∗a✝)
v_conF : (M, v)⊨Con (F (∗a✝) ℓ)
⊢ ∃ δ ∈ P (∗a✝) ℓ, relateSeq M δ v w

case test
W✝ : Type
M : KripkeModel W✝
v w : W✝
a✝ : Formula
v_γ_w : relate M (?'a✝) v w
ℓ : TP (?'a✝)
v_conF : (M, v)⊨Con (F (?'a✝) ℓ)
⊢ ∃ δ ∈ P (?'a✝) ℓ, relateSeq M δ v w