case union α β =>
  simp at v_γ_w
  cases v_γ_w
  case inl 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 ⟨δ, _⟩
    use δ
    simp_all [P]
  case inr 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 ⟨δ, _⟩
    use δ
    simp_all [P]
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
v_γ_w : relate M (α⋓β) v w
ℓ : TP (α⋓β)
v_conF : (M, v)⊨Con (F (α⋓β) ℓ)
⊢ ∃ δ ∈ P (α⋓β) ℓ, relateSeq M δ v w
no goals