case inl δ_in =>
  rcases δ_in with ⟨αs, αs_in, def_δ⟩
  subst def_δ
  simp_all
  cases γ_in
  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)
  case inr γ_in =>
    subst γ_in
    linarith
γ : Program
δ : List Program
γ_in : γ ∈ δ
α β : Program
ℓ : TP (α;'β)
δ_in : ∃ a ∈ List.filter (fun x => x != []) (P α fun τ => ℓ ⟨↑τ, ⋯⟩), a ++ [β] = δ
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β
no goals