. next hl =>
  simp only [insertUnit, hl, Prod.mk.eta, ite_true]
  exact h insertUnit_success
case isTrue
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, assignments, foundContradiction).snd.snd = true
⊢ ∃ j, (insertUnit (units, assignments, foundContradiction) l).snd.fst[j.val] = both

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
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