rw [insertUnit_fold_preserves_size]
n : Nat
assignments0 : Array Assignment
assignments0_size : assignments0.size = n
rupUnits : Array (Literal (PosFin n))
assignments : Array Assignment
assignments_size : assignments.size = n
b : Bool
units : List (Literal (PosFin n))
update_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  List.foldl insertUnit (rupUnits, assignments, b) units
⊢ update_res.snd.fst.size = n
n : Nat
assignments0 : Array Assignment
assignments0_size : assignments0.size = n
rupUnits : Array (Literal (PosFin n))
assignments : Array Assignment
assignments_size : assignments.size = n
b : Bool
units : List (Literal (PosFin n))
update_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  List.foldl insertUnit (rupUnits, assignments, b) units
⊢ assignments.size = n