∀ {n : ℕ} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n) (id : ℕ) (h : id < f.clauses.size) (idx : ℕ)
  (idx_in_bounds : idx < (f.clauses.toList.set id none).length), ↑⟨idx, ⋯⟩ < (f.clauses.set id none ⋯).toList.length