first
| ( rename_i rule
    cases rule
    <;> (simp at *; try rw [in_ress])
    case neg φ => simp [←Nat.add_assoc]
    case con φ ψ => simp; exact conDecreasesLength
    case ncon φ ψ =>
      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)))
| all_goals aesop
case LRnegR
res : SubPair
ϕ✝ : Formula
in_ress : res ∈ ∅
⊢ lengthOf res.1 < lengthOf {~ϕ✝} ∧ res.2 = ∅ ∨ lengthOf res.2 < lengthOf {ϕ✝} ∧ res.1 = ∅
no goals