cases em (ℓ ⟨τ, by simp [testsOfProgram]⟩)
φ τ : Formula
ℓ : TP (?'τ)
φ_in : φ ∈ if ℓ ⟨τ, ⋯⟩ = true then ∅ else [~τ]
⊢ lengthOfFormula φ < 2 + lengthOfFormula τ
case inl
φ τ : Formula
ℓ : TP (?'τ)
φ_in : φ ∈ if ℓ ⟨τ, ⋯⟩ = true then ∅ else [~τ]
h✝ : ℓ ⟨τ, ⋯⟩ = true
⊢ lengthOfFormula φ < 2 + lengthOfFormula τ

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