let acc0 := (units, assignments, foundContradiction)
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
h0 : foundContradiction = true → ∃ i, assignments[i.val] = both
insertUnit_fold_success : insertUnit_fold_res.snd.snd = true
⊢ ∃ j, insertUnit_fold_res.snd.fst[j.val] = both
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
h0 : foundContradiction = true → ∃ i, assignments[i.val] = both
insertUnit_fold_success : insertUnit_fold_res.snd.snd = true
acc0 : Array (Literal (PosFin n)) × Array Assignment × Bool := (units, assignments, foundContradiction)
⊢ ∃ j, insertUnit_fold_res.snd.fst[j.val] = both