simp_all [modelCanSemImplyForm, evaluatePoint, F, P, relateSeq, TP, testsOfProgram]
case intro.inr
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 τ
h✝ : ¬ℓ ⟨τ, ⋯⟩ = true
⊢ ∃ δ ∈ P (?'τ) ℓ, relateSeq M δ v w
no goals