have IH := P_goes_down γ_in δ_in
γ : Program
δ : List Program
γ_in : γ ∈ δ
α β : Program
ℓ : TP (α⋓β)
δ_in : δ ∈ P α fun τ => ℓ ⟨↑τ, ⋯⟩
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β
γ : Program
δ : List Program
γ_in : γ ∈ δ
α β : Program
ℓ : TP (α⋓β)
δ_in : δ ∈ P α fun τ => ℓ ⟨↑τ, ⋯⟩
IH :
  if isAtomic α = true then γ = α
  else if isStar α = true then lengthOfProgram γ ≤ lengthOfProgram α else lengthOfProgram γ < lengthOfProgram α
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β