rw [← hf.2]
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
assignments : Array Assignment := (f.insertRatUnits units).fst.assignments
⊢ assignments.size = n
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
assignments : Array Assignment := (f.insertRatUnits units).fst.assignments
⊢ assignments.size = f.assignments.size