have hsize : f.assignments.size = n := by rw [hf.2]
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
⊢ insertUnit_invariant f.assignments ⋯ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst
    (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).2.fst ⋯
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
hsize : f.assignments.size = n
⊢ insertUnit_invariant f.assignments ⋯ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst
    (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).2.fst ⋯