rcases δ_in with ⟨αs, αs_in, def_δ⟩
γ : Program
δ : List Program
γ_in : γ ∈ δ
α β : Program
ℓ : TP (α;'β)
δ_in : ∃ a ∈ List.filter (fun x => x != []) (P α fun τ => ℓ ⟨↑τ, ⋯⟩), a ++ [β] = δ
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β
case intro.intro
γ : Program
δ : List Program
γ_in : γ ∈ δ
α β : Program
ℓ : TP (α;'β)
αs : List Program
αs_in : αs ∈ List.filter (fun x => x != []) (P α fun τ => ℓ ⟨↑τ, ⋯⟩)
def_δ : αs ++ [β] = δ
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β