∀ {n : ℕ}
  (acc :
    Array Std.Tactic.BVDecide.LRAT.Internal.Assignment ×
      Std.Sat.CNF.Clause (Std.Tactic.BVDecide.LRAT.Internal.PosFin n) × Bool × Bool),
  acc.1.size = n →
    ∀ (l : Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)) (i : Fin n)
      (j1 j2 : Fin (List.length acc.2.1)),
      ↑l.1 ≠ ↑i →
        ∀ (k : Fin (List.length acc.2.1 + 1)) (zero_in_bounds : 0 < (l :: acc.2.1).length),
          k = ⟨0, zero_in_bounds⟩ → ¬↑((l :: acc.2.1).get k).1 = ↑i