simp only [clearRupUnits]
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
units : List (Literal (PosFin n))
⊢ (f.insertRupUnits units).fst.clearRupUnits = f
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 } =
    f