cases δ
γ : Program
δ : List Program
γ_in : γ ∈ δ
α : Program
ℓ : TP (∗α)
δ_in : δ = [] ∨ ∃ a ∈ List.filter (fun x => x != []) (P α fun x => ℓ ⟨↑x, ⋯⟩), a ++ [∗α] = δ
⊢ lengthOfProgram γ ≤ 1 + lengthOfProgram α
case nil
γ α : Program
ℓ : TP (∗α)
γ_in : γ ∈ []
δ_in : [] = [] ∨ ∃ a ∈ List.filter (fun x => x != []) (P α fun x => ℓ ⟨↑x, ⋯⟩), a ++ [∗α] = []
⊢ lengthOfProgram γ ≤ 1 + lengthOfProgram α

case cons
γ α : Program
ℓ : TP (∗α)
head✝ : Program
tail✝ : List Program
γ_in : γ ∈ head✝ :: tail✝
δ_in : head✝ :: tail✝ = [] ∨ ∃ a ∈ List.filter (fun x => x != []) (P α fun x => ℓ ⟨↑x, ⋯⟩), a ++ [∗α] = head✝ :: tail✝
⊢ lengthOfProgram γ ≤ 1 + lengthOfProgram α