∀ {n : ℕ} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n)
  (c : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n) (rupHints : Array ℕ)
  (f' : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n),
  (((f.insertRupUnits c.negate).1.performRupCheck rupHints).1, false) = (f', true) → f' = f.insert c