split at hl <;> simp_all (config := { decide := true })
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
assignments_l_ne_unassigned : (assignments.get ⟨l.fst.val, ⋯⟩ != unassigned) = true
l_eq_true : l.snd = true
hl :
  (match assignments.get ⟨l.fst.val, ⋯⟩ with
    | pos => true
    | neg => false
    | both => true
    | unassigned => false) =
    false
⊢ addAssignment true assignments[l.fst.val] = both
no goals