simp only [insertRupUnits]
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
units : List (Literal (PosFin n))
⊢ let assignments := (f.insertRupUnits units).fst.assignments;
  let_fun hsize := ⋯;
  let rupUnits := (f.insertRupUnits units).fst.rupUnits;
  insertUnit_invariant f.assignments ⋯ rupUnits assignments hsize
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
units : List (Literal (PosFin n))
⊢ insertUnit_invariant f.assignments ⋯ (List.foldl insertUnit (f.rupUnits, f.assignments, false) units).fst
    (List.foldl insertUnit (f.rupUnits, f.assignments, false) units).2.fst ⋯