rename relate M β v w => v_β_w
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
ℓ : TP (α;'β)
v_conF : (M, v)⊨Con (F (α;'β) ℓ)
v_Fℓα : evaluate M v (Con (F α fun τ => ℓ ⟨↑τ, ⋯⟩))
δ_in : [] ∈ P α fun τ => ℓ ⟨↑τ, ⋯⟩
v_α_u : relate M α v v
u_β_w : relate M β v w
⊢ ∃ δ ∈ P (α;'β) ℓ, relateSeq M δ v w
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
ℓ : TP (α;'β)
v_conF : (M, v)⊨Con (F (α;'β) ℓ)
v_Fℓα : evaluate M v (Con (F α fun τ => ℓ ⟨↑τ, ⋯⟩))
δ_in : [] ∈ P α fun τ => ℓ ⟨↑τ, ⋯⟩
v_α_u : relate M α v v
v_β_w : relate M β v w
⊢ ∃ δ ∈ P (α;'β) ℓ, relateSeq M δ v w