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