case test τ =>
  simp only [relate] at v_γ_w
  rcases v_γ_w with ⟨v_is_w, v_τ⟩
  cases em (ℓ ⟨τ, by simp [testsOfProgram]⟩ )
  all_goals
    simp_all [modelCanSemImplyForm, evaluatePoint, F, P, relateSeq, TP, testsOfProgram]
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
no goals