. next l_eq_true =>
  rw [l_eq_true]
  simp only [hasAssignment, l_eq_true, hasPosAssignment, getElem!, l_in_bounds, dite_true, ite_true,
    Bool.not_eq_true] at hl
  split at hl <;> simp_all (config := { decide := true })
case pos
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
assignments_l_ne_unassigned : (assignments.get ⟨l.fst.val, ⋯⟩ != unassigned) = true
h✝ : l.snd = true
⊢ addAssignment l.snd assignments[l.fst.val] = both

case neg
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
assignments_l_ne_unassigned : (assignments.get ⟨l.fst.val, ⋯⟩ != unassigned) = true
h✝ : ¬l.snd = true
⊢ addAssignment l.snd assignments[l.fst.val] = both
case neg
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
assignments_l_ne_unassigned : (assignments.get ⟨l.fst.val, ⋯⟩ != unassigned) = true
h✝ : ¬l.snd = true
⊢ addAssignment l.snd assignments[l.fst.val] = both