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