∀ {n : ℕ} (clauses : Array (Option (Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n))) (id : ℕ)
  (c : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n), clauses[id]? = some (some c) → id < clauses.size