all_goals
  simp only [F, List.mem_union_iff, lengthOfProgram] at *
case atom_prog
φ : Formula
a✝ : ℕ
ℓ : TP (·a✝)
φ_in : φ ∈ F (·a✝) ℓ
⊢ lengthOfFormula φ < lengthOfProgram (·a✝)

case sequence
φ : Formula
a✝¹ a✝ : Program
ℓ : TP (a✝¹;'a✝)
φ_in : φ ∈ F (a✝¹;'a✝) ℓ
⊢ lengthOfFormula φ < lengthOfProgram (a✝¹;'a✝)

case union
φ : Formula
a✝¹ a✝ : Program
ℓ : TP (a✝¹⋓a✝)
φ_in : φ ∈ F (a✝¹⋓a✝) ℓ
⊢ lengthOfFormula φ < lengthOfProgram (a✝¹⋓a✝)

case star
φ : Formula
a✝ : Program
ℓ : TP (∗a✝)
φ_in : φ ∈ F (∗a✝) ℓ
⊢ lengthOfFormula φ < lengthOfProgram (∗a✝)

case test
φ a✝ : Formula
ℓ : TP (?'a✝)
φ_in : φ ∈ F (?'a✝) ℓ
⊢ lengthOfFormula φ < lengthOfProgram (?'a✝)
case atom_prog
φ : Formula
a✝ : ℕ
ℓ : TP (·a✝)
φ_in : φ ∈ ∅
⊢ lengthOfFormula φ < 1

case sequence
φ : Formula
a✝¹ a✝ : Program
ℓ : TP (a✝¹;'a✝)
φ_in : (φ ∈ F a✝¹ fun τ => ℓ ⟨↑τ, ⋯⟩) ∨ φ ∈ F a✝ fun τ => ℓ ⟨↑τ, ⋯⟩
⊢ lengthOfFormula φ < 1 + lengthOfProgram a✝¹ + lengthOfProgram a✝

case union
φ : Formula
a✝¹ a✝ : Program
ℓ : TP (a✝¹⋓a✝)
φ_in : (φ ∈ F a✝¹ fun τ => ℓ ⟨↑τ, ⋯⟩) ∨ φ ∈ F a✝ fun τ => ℓ ⟨↑τ, ⋯⟩
⊢ lengthOfFormula φ < 1 + lengthOfProgram a✝¹ + lengthOfProgram a✝

case star
φ : Formula
a✝ : Program
ℓ : TP (∗a✝)
φ_in : φ ∈ F a✝ fun x => ℓ ⟨↑x, ⋯⟩
⊢ lengthOfFormula φ < 1 + lengthOfProgram a✝

case test
φ a✝ : Formula
ℓ : TP (?'a✝)
φ_in : φ ∈ if ℓ ⟨a✝, ⋯⟩ = true then ∅ else [~a✝]
⊢ lengthOfFormula φ < 2 + lengthOfFormula a✝