∀ {n : ℕ} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n),
  f.ratUnits = #[] ∧ f.assignments.size = n →
    ∀ (p : Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)) (ratHints : Array (ℕ × Array ℕ))
      (i : Fin ratHints.size),
      (Array.foldl (fun acc ratHint => if acc.2 = true then acc.1.performRatCheck p ratHint else (acc.1, false))
              (f, true) ratHints).2 =
          true →
        (f.performRatCheck p ratHints[i]).2 = true