simp only [l_eq_i, Array.get_modify_at_idx i_in_bounds, h]
n : Nat
assignments : Array Assignment
assignments_size : assignments.size = n
units : Array (Literal (PosFin n))
foundContradiction : Bool
l : Literal (PosFin n)
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  insertUnit (units, assignments, foundContradiction) l
h✝ : foundContradiction = true → ∃ i, assignments[i.val] = both
l_in_bounds : l.fst.val < assignments.size
hl : ¬hasAssignment l.snd assignments[l.fst.val]! = true
foundContradiction_eq_true : foundContradiction = true
i : PosFin n
h : assignments[i.val] = both
i_in_bounds : i.val < assignments.size
l_eq_i : l.fst.val = i.val
⊢ (assignments.modify l.fst.val (addAssignment l.snd))[i.val] = both
n : Nat
assignments : Array Assignment
assignments_size : assignments.size = n
units : Array (Literal (PosFin n))
foundContradiction : Bool
l : Literal (PosFin n)
insertUnit_res : Array (Literal (PosFin n)) × Array Assignment × Bool :=
  insertUnit (units, assignments, foundContradiction) l
h✝ : foundContradiction = true → ∃ i, assignments[i.val] = both
l_in_bounds : l.fst.val < assignments.size
hl : ¬hasAssignment l.snd assignments[l.fst.val]! = true
foundContradiction_eq_true : foundContradiction = true
i : PosFin n
h : assignments[i.val] = both
i_in_bounds : i.val < assignments.size
l_eq_i : l.fst.val = i.val
⊢ addAssignment l.snd both = both