∀ {n : ℕ} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n),
  f.assignments.size = n →
    ∀ (assignments : Array Std.Tactic.BVDecide.LRAT.Internal.Assignment),
      assignments.size = n →
        ∀ (derivedLits : Std.Sat.CNF.Clause (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)) (i : Fin n),
          ↑i < n → ↑i < assignments.size