case atom_prog =>
  simp [F, P, relateSeq] at *
  exact v_γ_w
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
no goals