linarith
case inr.inr
γ α : Program
ℓ : TP (∗α)
head✝ : Program
tail✝ αs : List Program
γ_in✝ : γ = head✝ ∨ γ ∈ tail✝
αs_in : αs ∈ List.filter (fun x => x != []) (P α fun x => ℓ ⟨↑x, ⋯⟩)
def_δ : αs ++ [∗α] = head✝ :: tail✝
γ_in : γ ∈ αs
IH : lengthOfProgram γ < lengthOfProgram α
h✝¹ : isAtomic α = false
h✝ : isStar α = false
⊢ lengthOfProgram γ ≤ 1 + lengthOfProgram α
no goals