case union α β =>
  cases δ_in
  case inl δ_in =>
    have IH := P_goes_down γ_in δ_in
    cases em (isAtomic α) <;> cases em (isStar α)
    all_goals (simp_all;try linarith)
  case inr δ_in =>
    have IH := P_goes_down γ_in δ_in
    cases em (isAtomic β) <;> cases em (isStar β)
    all_goals (simp_all;try linarith)
γ : Program
δ : List Program
γ_in : γ ∈ δ
α β : Program
ℓ : TP (α⋓β)
δ_in : (δ ∈ P α fun τ => ℓ ⟨↑τ, ⋯⟩) ∨ δ ∈ P β fun τ => ℓ ⟨↑τ, ⋯⟩
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β
no goals