case inl γ_in =>
  have IH := P_goes_down γ_in (List.mem_of_mem_filter αs_in)
  cases em (isAtomic α) <;> cases em (isStar α)
  all_goals (simp_all;try linarith)
γ α : Program
ℓ : TP (∗α)
head✝ : Program
tail✝ : List Program
γ_in✝ : γ ∈ head✝ :: tail✝
αs : List Program
αs_in : αs ∈ List.filter (fun x => x != []) (P α fun x => ℓ ⟨↑x, ⋯⟩)
def_δ : αs ++ [∗α] = head✝ :: tail✝
γ_in : γ ∈ αs
⊢ lengthOfProgram γ ≤ 1 + lengthOfProgram α
no goals