∀ {n : ℕ} (assignments : Array Std.Tactic.BVDecide.LRAT.Internal.Assignment)
  (l : Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)),
  ↑l.1 + 1 ≤ assignments.size → ↑l.1 < assignments.size