have IHα := F_goes_down φ_in
φ : Formula
α : Program
ℓ : TP (∗α)
φ_in : φ ∈ F α fun x => ℓ ⟨↑x, ⋯⟩
⊢ lengthOfFormula φ < 1 + lengthOfProgram α
φ : Formula
α : Program
ℓ : TP (∗α)
φ_in : φ ∈ F α fun x => ℓ ⟨↑x, ⋯⟩
IHα : lengthOfFormula φ < lengthOfProgram α
⊢ lengthOfFormula φ < 1 + lengthOfProgram α