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