exact insertUnit_fold_preserves_size f.ratUnits f.assignments false
n : Nat
f : DefaultFormula n
units : List (Literal (PosFin n))
⊢ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).2.fst.size = f.assignments.size
no goals