case inl hyp =>
  subst hyp
  simp [relateSeq] at v_δ_u
  subst v_δ_u
  rename relate M β v w => v_β_w
  have v_Fℓβ : evaluate M v (Con (F β ℓ)) := by simp_all [conEval, F, modelCanSemImplyForm, evaluatePoint]
  have IHβ := existsBoxFP β v_β_w ℓ v_Fℓβ rcases IHβ with ⟨η, ⟨η_in, v_η_w⟩⟩
  use η
  simp_all [P]
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
ℓ : TP (α;'β)
v_conF : (M, v)⊨Con (F (α;'β) ℓ)
u : W✝
v_α_u : relate M α v u
u_β_w : relate M β u w
v_Fℓα : evaluate M v (Con (F α fun τ => ℓ ⟨↑τ, ⋯⟩))
δ : List Program
δ_in : δ ∈ P α fun τ => ℓ ⟨↑τ, ⋯⟩
v_δ_u : relateSeq M δ v u
hyp : δ = []
⊢ ∃ δ ∈ P (α;'β) ℓ, relateSeq M δ v w
no goals