case union α β =>
  cases φ_in
  case inl φ_in_Fα =>
    have IHα := F_goes_down φ_in_Fα
    linarith
  case inr φ_in_Fβ =>
    have IHβ := F_goes_down φ_in_Fβ
    linarith
φ : Formula
α β : Program
ℓ : TP (α⋓β)
φ_in : (φ ∈ F α fun τ => ℓ ⟨↑τ, ⋯⟩) ∨ φ ∈ F β fun τ => ℓ ⟨↑τ, ⋯⟩
⊢ lengthOfFormula φ < 1 + lengthOfProgram α + lengthOfProgram β
no goals