( simp [case_phi]
  rw [Nat.add_comm 1 (lengthOfFormula φ), Nat.add_assoc]
  aesop)
case inl
res : SubPair
φ ψ : Formula
case_phi : res = (∅, {~φ})
⊢ res.2.sum lengthOfFormula < 1 + (1 + lengthOfFormula φ + lengthOfFormula ψ) ∧ res.1 = ∅
no goals