cases α
φ : Formula
α : Program
ℓ : TP α
φ_in : φ ∈ F α ℓ
⊢ lengthOfFormula φ < lengthOfProgram α
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✝)