have IH := P_goes_down γ_in (List.mem_of_mem_filter αs_in)
γ α : Program
ℓ : TP (∗α)
head✝ : Program
tail✝ : List Program
γ_in✝ : γ ∈ head✝ :: tail✝
αs : List Program
αs_in : αs ∈ List.filter (fun x => x != []) (P α fun x => ℓ ⟨↑x, ⋯⟩)
def_δ : αs ++ [∗α] = head✝ :: tail✝
γ_in : γ ∈ αs
⊢ lengthOfProgram γ ≤ 1 + lengthOfProgram α
γ α : Program
ℓ : TP (∗α)
head✝ : Program
tail✝ : List Program
γ_in✝ : γ ∈ head✝ :: tail✝
αs : List Program
αs_in : αs ∈ List.filter (fun x => x != []) (P α fun x => ℓ ⟨↑x, ⋯⟩)
def_δ : αs ++ [∗α] = head✝ :: tail✝
γ_in : γ ∈ αs
IH :
  if isAtomic α = true then γ = α
  else if isStar α = true then lengthOfProgram γ ≤ lengthOfProgram α else lengthOfProgram γ < lengthOfProgram α
⊢ lengthOfProgram γ ≤ 1 + lengthOfProgram α