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