. next hl =>
  simp only [Bool.or_eq_true] at insertUnit_success
  rcases insertUnit_success with foundContradiction_eq_true | assignments_l_ne_unassigned
  . simp only [insertUnit, hl, Prod.mk.eta, ite_false]
    rcases h foundContradiction_eq_true with ⟨i, h⟩
    have i_in_bounds : i.1 < assignments.size := by rw [assignments_size]; exact i.2.2
    apply Exists.intro i
    by_cases l.1.1 = i.1
    . next l_eq_i =>
      simp only [l_eq_i, Array.get_modify_at_idx i_in_bounds, h]
      exact add_of_both_eq_both l.2
    . next l_ne_i =>
      rw [Array.get_modify_unchanged l_in_bounds i_in_bounds _ l_ne_i]
      exact h
  . apply Exists.intro l.1
    simp only [insertUnit, hl, Prod.mk.eta, ite_false, Array.get_modify_at_idx l_in_bounds]
    simp only [getElem!, l_in_bounds, dite_true] at assignments_l_ne_unassigned
    by_cases l.2
    . 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 })
    . next l_eq_false =>
      simp only [Bool.not_eq_true] at l_eq_false
      rw [l_eq_false]
      simp only [hasAssignment, l_eq_false, hasNegAssignment, getElem!, l_in_bounds, dite_true, ite_false,
        Bool.not_eq_true] at hl
      split at hl <;> simp_all (config := { decide := true })
case isFalse
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
h✝ : ¬hasAssignment l.snd assignments[l.fst.val]! = true
insertUnit_success :
  (units.push l, assignments.modify l.fst.val (addAssignment l.snd),
          foundContradiction || assignments[l.fst.val]! != unassigned).snd.snd =
    true
⊢ ∃ j, (insertUnit (units, assignments, foundContradiction) l).snd.fst[j.val] = both
no goals