simp_all only [false_or]
γ α : 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 α
γ α : Program
ℓ : TP (∗α)
head✝ : Program
tail✝ : List Program
γ_in : γ ∈ head✝ :: tail✝
δ_in : ∃ a ∈ List.filter (fun x => x != []) (P α fun x => ℓ ⟨↑x, ⋯⟩), a ++ [∗α] = head✝ :: tail✝
⊢ lengthOfProgram γ ≤ 1 + lengthOfProgram α