case star α =>
  cases δ
  case nil =>
    exfalso; cases γ_in
  case cons =>
    simp_all only [false_or]
    rcases δ_in with ⟨αs, αs_in, def_δ⟩
    subst_eqs
    cases em (γ ∈ αs)
    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 γ_not_in =>
      have : γ = (∗α) := by rw [← def_δ] at γ_in; simp at γ_in; tauto
      subst_eqs
      simp
γ : Program
δ : List Program
γ_in : γ ∈ δ
α : Program
ℓ : TP (∗α)
δ_in : δ = [] ∨ ∃ a ∈ List.filter (fun x => x != []) (P α fun x => ℓ ⟨↑x, ⋯⟩), a ++ [∗α] = δ
⊢ lengthOfProgram γ ≤ 1 + lengthOfProgram α
no goals