simp only [insertRupUnits, Prod.mk.eta]
n : Nat
f : DefaultFormula n
units : List (Literal (PosFin n))
⊢ (f.insertRupUnits units).fst.assignments.size = f.assignments.size
n : Nat
f : DefaultFormula n
units : List (Literal (PosFin n))
⊢ (List.foldl insertUnit (f.rupUnits, f.assignments, false) units).2.fst.size = f.assignments.size