∀ {n : ℕ} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n),
  f.ReadyForRupAdd →
    ∀ (c : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n) (i : Std.Tactic.BVDecide.LRAT.Internal.PosFin n),
      ↑⟨↑i, ⋯⟩ <
        (List.foldl Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.insertUnit (f.rupUnits, f.assignments, false)
                c.negate).2.1.size