∀ {rupHints : Array ℕ} {n : ℕ} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n)
  (f_assignments_size : f.assignments.size = n) (f' : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n),
  f' = (f.performRupCheck rupHints).1 →
    ∀ (f'_assignments_size : f'.assignments.size = n)
      (derivedLits : Std.Sat.CNF.Clause (Std.Tactic.BVDecide.LRAT.Internal.PosFin n))
      (derivedLits_arr : Array (Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n))),
      derivedLits_arr = { toList := derivedLits } →
        f.DerivedLitsInvariant f_assignments_size f'.assignments f'_assignments_size derivedLits →
          (∀ (i j : Fin derivedLits_arr.size), i ≠ j → derivedLits_arr[i] ≠ derivedLits_arr[j]) →
            f.ClearInsertInductionMotive f_assignments_size derivedLits_arr 0 f'.assignments