cases rule <;>
( 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)
Lcond Rcond : Finset Formula
ress : List SubPair
rule : LocalRule (Lcond, Rcond) ress
res : SubPair
in_ress : res ∈ ress
⊢ lengthOf res.1 < lengthOf Lcond ∧ res.2 = ∅ ∨ lengthOf res.2 < lengthOf Rcond ∧ res.1 = ∅
no goals