∀ {n : ℕ} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n)
  (c : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n),
  f.ReadyForRupAdd →
    ∀ (l : Std.Tactic.BVDecide.LRAT.Internal.PosFin n)
      (hsize : (f.assignments.modify (↑l) Std.Tactic.BVDecide.LRAT.Internal.Assignment.addPosAssignment).size = n)
      (i : Std.Tactic.BVDecide.LRAT.Internal.PosFin n) (b : Bool),
      Std.Tactic.BVDecide.LRAT.Internal.Assignment.hasAssignment b
            (f.assignments.modify (↑l) Std.Tactic.BVDecide.LRAT.Internal.Assignment.addPosAssignment)[↑i] =
          true →
        ∀ (i_in_bounds : ↑i < f.assignments.size),
          ¬↑l = ↑i → Std.Tactic.BVDecide.LRAT.Internal.Assignment.hasAssignment b f.assignments[↑i] = true