have v_Fℓβ : evaluate M v (Con (F β ℓ)) := by simp_all [conEval, F, modelCanSemImplyForm, evaluatePoint]
case intro.intro.intro.intro
W✝ : Type
M : KripkeModel W✝
v w : W✝
β : Program
ℓ : TP (∗β)
v_conF : (M, v)⊨Con (F (∗β) ℓ)
v_γ_w : Relation.ReflTransGen (relate M β) v w
v_neq_w : v ≠ w
u : W✝
v_neq_u : v ≠ u
v_β_u : relate M β v u
u_βS_w : Relation.ReflTransGen (relate M β) u w
⊢ ∃ δ ∈ P (∗β) ℓ, relateSeq M δ v w
case intro.intro.intro.intro
W✝ : Type
M : KripkeModel W✝
v w : W✝
β : Program
ℓ : TP (∗β)
v_conF : (M, v)⊨Con (F (∗β) ℓ)
v_γ_w : Relation.ReflTransGen (relate M β) v w
v_neq_w : v ≠ w
u : W✝
v_neq_u : v ≠ u
v_β_u : relate M β v u
u_βS_w : Relation.ReflTransGen (relate M β) u w
v_Fℓβ :
  evaluate M v
    (Con
      (F β fun x =>
        match x with
        | ⟨f, f_in⟩ => ℓ ⟨f, ⋯⟩))
⊢ ∃ δ ∈ P (∗β) ℓ, relateSeq M δ v w