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
ℓ : TP (∗α)
head✝ : Program
tail✝ : List Program
γ_in : γ ∈ head✝ :: tail✝
δ_in : head✝ :: tail✝ = [] ∨ ∃ a ∈ List.filter (fun x => x != []) (P α fun x => ℓ ⟨↑x, ⋯⟩), a ++ [∗α] = head✝ :: tail✝
⊢ lengthOfProgram γ ≤ 1 + lengthOfProgram α
no goals