∀ {n : ℕ} (arr : Array (Option (Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n))) (i : ℕ),
  i + 1 ≤ (Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.ofArray arr).rupUnits.size →
    i < (Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.ofArray arr).rupUnits.size