∀ {n : ℕ} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n)
  (c : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n) (i : ℕ),
  i + 1 ≤
      (match c.isUnit with
          | none =>
            { clauses := f.clauses.push (some c), rupUnits := f.rupUnits, ratUnits := f.ratUnits,
              assignments := f.assignments }
          | some (l, true) =>
            { clauses := f.clauses.push (some c), rupUnits := f.rupUnits, ratUnits := f.ratUnits,
              assignments := f.assignments.modify (↑l) Std.Tactic.BVDecide.LRAT.Internal.Assignment.addPosAssignment }
          | some (l, false) =>
            { clauses := f.clauses.push (some c), rupUnits := f.rupUnits, ratUnits := f.ratUnits,
              assignments :=
                f.assignments.modify (↑l)
                  Std.Tactic.BVDecide.LRAT.Internal.Assignment.addNegAssignment }).ratUnits.size →
    i <
      (match c.isUnit with
          | none =>
            { clauses := f.clauses.push (some c), rupUnits := f.rupUnits, ratUnits := f.ratUnits,
              assignments := f.assignments }
          | some (l, true) =>
            { clauses := f.clauses.push (some c), rupUnits := f.rupUnits, ratUnits := f.ratUnits,
              assignments := f.assignments.modify (↑l) Std.Tactic.BVDecide.LRAT.Internal.Assignment.addPosAssignment }
          | some (l, false) =>
            { clauses := f.clauses.push (some c), rupUnits := f.rupUnits, ratUnits := f.ratUnits,
              assignments :=
                f.assignments.modify (↑l) Std.Tactic.BVDecide.LRAT.Internal.Assignment.addNegAssignment }).ratUnits.size