cases φ_in
φ : Formula
α β : Program
ℓ : TP (α;'β)
φ_in : (φ ∈ F α fun τ => ℓ ⟨↑τ, ⋯⟩) ∨ φ ∈ F β fun τ => ℓ ⟨↑τ, ⋯⟩
⊢ lengthOfFormula φ < 1 + lengthOfProgram α + lengthOfProgram β
case inl
φ : Formula
α β : Program
ℓ : TP (α;'β)
h✝ : φ ∈ F α fun τ => ℓ ⟨↑τ, ⋯⟩
⊢ lengthOfFormula φ < 1 + lengthOfProgram α + lengthOfProgram β

case inr
φ : Formula
α β : Program
ℓ : TP (α;'β)
h✝ : φ ∈ F β fun τ => ℓ ⟨↑τ, ⋯⟩
⊢ lengthOfFormula φ < 1 + lengthOfProgram α + lengthOfProgram β