simp_all
case inl
γ : Program
δ : List Program
γ_in : γ ∈ δ
α β : Program
ℓ : TP (α;'β)
δ_in : δ ∈ if [] ∈ P α fun τ => ℓ ⟨↑τ, ⋯⟩ then P β fun τ => ℓ ⟨↑τ, ⋯⟩ else []
h✝ : [] ∈ P α fun τ => ℓ ⟨↑τ, ⋯⟩
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β
case inl
γ : Program
δ : List Program
γ_in : γ ∈ δ
α β : Program
ℓ : TP (α;'β)
δ_in : δ ∈ P β fun τ => ℓ ⟨↑τ, ⋯⟩
h✝ : [] ∈ P α fun τ => ℓ ⟨↑τ, ⋯⟩
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β