∀ {n : ℕ}
  (acc :
    Array Std.Tactic.BVDecide.LRAT.Internal.Assignment ×
      Std.Sat.CNF.Clause (Std.Tactic.BVDecide.LRAT.Internal.PosFin n) × Bool × Bool)
  (l : Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)) (j : Fin (List.length acc.2.1)),
  ↑j + 2 ≤ (l :: acc.2.1).length → ↑j + 1 < (l :: acc.2.1).length