∀ {n : ℕ} (acc : Array Std.Tactic.BVDecide.LRAT.Internal.Assignment) (i : Std.Tactic.BVDecide.LRAT.Internal.PosFin n)
  (c : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n),
  (Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.ofArray_fold_fn acc (some c)).size = n →
    ∀ (l : Std.Tactic.BVDecide.LRAT.Internal.PosFin n),
      c.isUnit = some (l, false) →
        ↑i < (acc.modify (↑l) Std.Tactic.BVDecide.LRAT.Internal.Assignment.addNegAssignment).size