∀ {n : ℕ} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n),
  f.ReadyForRatAdd →
    ∀ (c : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n)
      (pivot : Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)) (rupHints : Array ℕ)
      (ratHints : Array (ℕ × Array ℕ)),
      pivot ∈ Std.Tactic.BVDecide.LRAT.Internal.Clause.toList c →
        f.ratHintsExhaustive pivot ratHints = true →
          (Array.foldl (fun x ratHint => if x.2 = true then x.1.performRatCheck pivot.negate ratHint else (x.1, false))
                  (((f.insertRupUnits c.negate).1.performRupCheck rupHints).1, true) ratHints).2 =
              true →
            Std.Tactic.BVDecide.LRAT.Internal.Equisat (Std.Tactic.BVDecide.LRAT.Internal.PosFin n) f (f.insert c)