all_goals (simp_all;try linarith)
case inl.inl
γ α β : Program
ℓ : TP (α;'β)
αs : List Program
αs_in : αs ∈ List.filter (fun x => x != []) (P α fun τ => ℓ ⟨↑τ, ⋯⟩)
γ_in : γ ∈ αs
IH :
  if isAtomic α = true then γ = α
  else if isStar α = true then lengthOfProgram γ ≤ lengthOfProgram α else lengthOfProgram γ < lengthOfProgram α
h✝¹ : isAtomic α = true
h✝ : isStar α = true
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β

case inl.inr
γ α β : Program
ℓ : TP (α;'β)
αs : List Program
αs_in : αs ∈ List.filter (fun x => x != []) (P α fun τ => ℓ ⟨↑τ, ⋯⟩)
γ_in : γ ∈ αs
IH :
  if isAtomic α = true then γ = α
  else if isStar α = true then lengthOfProgram γ ≤ lengthOfProgram α else lengthOfProgram γ < lengthOfProgram α
h✝¹ : isAtomic α = true
h✝ : ¬isStar α = true
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β

case inr.inl
γ α β : Program
ℓ : TP (α;'β)
αs : List Program
αs_in : αs ∈ List.filter (fun x => x != []) (P α fun τ => ℓ ⟨↑τ, ⋯⟩)
γ_in : γ ∈ αs
IH :
  if isAtomic α = true then γ = α
  else if isStar α = true then lengthOfProgram γ ≤ lengthOfProgram α else lengthOfProgram γ < lengthOfProgram α
h✝¹ : ¬isAtomic α = true
h✝ : isStar α = true
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β

case inr.inr
γ α β : Program
ℓ : TP (α;'β)
αs : List Program
αs_in : αs ∈ List.filter (fun x => x != []) (P α fun τ => ℓ ⟨↑τ, ⋯⟩)
γ_in : γ ∈ αs
IH :
  if isAtomic α = true then γ = α
  else if isStar α = true then lengthOfProgram γ ≤ lengthOfProgram α else lengthOfProgram γ < lengthOfProgram α
h✝¹ : ¬isAtomic α = true
h✝ : ¬isStar α = true
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β
no goals