( 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)))
case LRnegR
res : SubPair
ϕ✝ : Formula
in_ress : res ∈ ∅
⊢ lengthOf res.1 < lengthOf {~ϕ✝} ∧ res.2 = ∅ ∨ lengthOf res.2 < lengthOf {ϕ✝} ∧ res.1 = ∅
no goals