simp only [relate] at v_γ_w
W✝ : Type
M : KripkeModel W✝
v w : W✝
τ : Formula
v_γ_w : relate M (?'τ) v w
ℓ : TP (?'τ)
v_conF : (M, v)⊨Con (F (?'τ) ℓ)
⊢ ∃ δ ∈ P (?'τ) ℓ, relateSeq M δ v w
W✝ : Type
M : KripkeModel W✝
v w : W✝
τ : Formula
ℓ : TP (?'τ)
v_conF : (M, v)⊨Con (F (?'τ) ℓ)
v_γ_w : v = w ∧ evaluate M v τ
⊢ ∃ δ ∈ P (?'τ) ℓ, relateSeq M δ v w