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