try rw [in_ress]
case oneSidedR.con
res : SubPair
φ✝ ψ✝ : Formula
in_ress : res = (∅, {φ✝, ψ✝})
⊢ res.2.sum lengthOfFormula < 1 + lengthOfFormula φ✝ + lengthOfFormula ψ✝ ∧ res.1 = ∅
case oneSidedR.con
res : SubPair
φ✝ ψ✝ : Formula
in_ress : res = (∅, {φ✝, ψ✝})
⊢ (∅, {φ✝, ψ✝}).2.sum lengthOfFormula < 1 + lengthOfFormula φ✝ + lengthOfFormula ψ✝ ∧ (∅, {φ✝, ψ✝}).1 = ∅