∀ {n : ℕ} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n) (ratHints : Array (ℕ × Array ℕ))
  (j : Fin (Array.map (fun x => x.1) ratHints).toList.length) (j_in_bounds : ↑j < ratHints.size),
  ratHints[⟨↑j, ⋯⟩].1 + 1 ≤ f.clauses.size → ratHints[⟨↑j, ⋯⟩].1 < f.clauses.size