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