∀ {n : ℕ} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n)
  (units : Std.Sat.CNF.Clause (Std.Tactic.BVDecide.LRAT.Internal.PosFin n))
  (w : Fin (f.insertRatUnits units).1.ratUnits.size), ↑w < (f.insertRatUnits units).1.ratUnits.size