rw [assignments_size]
n : Nat
assignments : Array Assignment
assignments_size : assignments.size = n
units : Array (Literal (PosFin n))
foundContradiction : Bool
l : List (Literal (PosFin n))
insertUnit_fold_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  List.foldl insertUnit (units, assignments, foundContradiction) l
i : PosFin n
⊢ i.val < assignments.size
n : Nat
assignments : Array Assignment
assignments_size : assignments.size = n
units : Array (Literal (PosFin n))
foundContradiction : Bool
l : List (Literal (PosFin n))
insertUnit_fold_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  List.foldl insertUnit (units, assignments, foundContradiction) l
i : PosFin n
⊢ i.val < n