(simp_all;try linarith)
case inr.inr
γ : Program
δ : List Program
γ_in : γ ∈ δ
α β : Program
ℓ : TP (α⋓β)
δ_in : δ ∈ P β fun τ => ℓ ⟨↑τ, ⋯⟩
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