rw [← f_readyForRupAdd.2.1]
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
units : List (Literal (PosFin n))
assignments : Array Assignment := (f.insertRupUnits units).fst.assignments
⊢ assignments.size = n
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
units : List (Literal (PosFin n))
assignments : Array Assignment := (f.insertRupUnits units).fst.assignments
⊢ assignments.size = f.assignments.size