rcases v_γ_w with ⟨u, v_α_u, u_β_w⟩
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
ℓ : TP (α;'β)
v_conF : (M, v)⊨Con (F (α;'β) ℓ)
v_γ_w : ∃ y, relate M α v y ∧ relate M β y w
⊢ ∃ δ ∈ P (α;'β) ℓ, relateSeq M δ v w
case intro.intro
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
ℓ : TP (α;'β)
v_conF : (M, v)⊨Con (F (α;'β) ℓ)
u : W✝
v_α_u : relate M α v u
u_β_w : relate M β u w
⊢ ∃ δ ∈ P (α;'β) ℓ, relateSeq M δ v w