simp only
case assignments
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
units : List (Literal (PosFin n))
⊢ { clauses := (f.insertRupUnits units).1.clauses, rupUnits := #[], ratUnits := (f.insertRupUnits units).1.ratUnits,
        assignments :=
          Array.foldl clearUnit (f.insertRupUnits units).1.assignments (f.insertRupUnits units).1.rupUnits
            0 }.assignments =
    f.assignments
case assignments
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
units : List (Literal (PosFin n))
⊢ Array.foldl clearUnit (f.insertRupUnits units).1.assignments (f.insertRupUnits units).1.rupUnits 0 = f.assignments