rcases v_γ_w with ⟨v_is_w, v_τ⟩
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
case intro
W✝ : Type
M : KripkeModel W✝
v w : W✝
τ : Formula
ℓ : TP (?'τ)
v_conF : (M, v)⊨Con (F (?'τ) ℓ)
v_is_w : v = w
v_τ : evaluate M v τ
⊢ ∃ δ ∈ P (?'τ) ℓ, relateSeq M δ v w