simp only [F, List.mem_union_iff, lengthOfProgram] at *
case test
φ a✝ : Formula
ℓ : TP (?'a✝)
φ_in : φ ∈ F (?'a✝) ℓ
⊢ lengthOfFormula φ < lengthOfProgram (?'a✝)
case test
φ a✝ : Formula
ℓ : TP (?'a✝)
φ_in : φ ∈ if ℓ ⟨a✝, ⋯⟩ = true then ∅ else [~a✝]
⊢ lengthOfFormula φ < 2 + lengthOfFormula a✝