∀ {n : ℕ} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n)
  (units : Std.Sat.CNF.Clause (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)),
  (f.insertRupUnits units).1.assignments.size = f.assignments.size