have hsize : f.assignments.size = n := by rw [f_readyForRupAdd.2.1]
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 ⋯
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
units : List (Literal (PosFin n))
hsize : f.assignments.size = 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 ⋯