have IHβ := F_goes_down φ_in_Fβ
φ : Formula
α β : Program
ℓ : TP (α;'β)
φ_in_Fβ : φ ∈ F β fun τ => ℓ ⟨↑τ, ⋯⟩
⊢ lengthOfFormula φ < 1 + lengthOfProgram α + lengthOfProgram β
φ : Formula
α β : Program
ℓ : TP (α;'β)
φ_in_Fβ : φ ∈ F β fun τ => ℓ ⟨↑τ, ⋯⟩
IHβ : lengthOfFormula φ < lengthOfProgram β
⊢ lengthOfFormula φ < 1 + lengthOfProgram α + lengthOfProgram β