. intro k k_ne_j1 k_ne_j2
  by_cases k.1 < units.size
  . next k_in_bounds =>
    have k_ne_j1 : ⟨k.1, k_in_bounds⟩ ≠ j1 := by
      intro k_eq_j1
      simp only [← k_eq_j1, not_true] at k_ne_j1
    have k_ne_j2 : ⟨k.1, k_in_bounds⟩ ≠ j2 := by
      intro k_eq_j2
      simp only [← k_eq_j2, not_true] at k_ne_j2
    split
    . exact h5 ⟨k.1, k_in_bounds⟩ k_ne_j1 k_ne_j2
    . simp only [ne_eq]
      rw [Array.get_push]
      simp only [k_in_bounds, dite_true]
      exact h5 ⟨k.1, k_in_bounds⟩ k_ne_j1 k_ne_j2
  . next k_not_lt_units_size =>
    split
    . next h =>
      exfalso
      have k_property := k.2
      simp only [insertUnit, h, Prod.mk.eta, ite_true] at k_property
      exact k_not_lt_units_size k_property
    . next h =>
      simp only
      have k_eq_units_size : k.1 = units.size := by
        have k_property := k.2
        simp only [insertUnit, h, Prod.mk.eta, ite_false, Array.size_push] at k_property
        rcases Nat.lt_or_eq_of_le $ Nat.le_of_lt_succ k_property with k_lt_units_size | k_eq_units_size
        . exfalso; exact k_not_lt_units_size k_lt_units_size
        . exact k_eq_units_size
      simp only [k_eq_units_size, Array.get_push_eq, ne_eq]
      intro l_eq_i
      simp [getElem!, l_eq_i, i_in_bounds, h3, has_of_both] at h
case inr.inr.intro.intro.intro.intro.intro.intro.intro.right.right.right.right
n : Nat
assignments0 : Array Assignment
assignments0_size : assignments0.size = n
units : Array (Literal (PosFin n))
assignments : Array Assignment
assignments_size : assignments.size = n
foundContradiction : Bool
l : Literal (PosFin n)
i : Fin n
i_in_bounds : ↑i < assignments.size
l_in_bounds : l.fst.val < assignments.size
j1 j2 : Fin units.size
i_gt_zero : ↑i > 0
h1 : units[↑j1] = (⟨↑i, ⋯⟩, true)
h2 : units[↑j2] = (⟨↑i, ⋯⟩, false)
h3 : assignments[↑i] = both
h4 : assignments0[↑i] = unassigned
h5 : ∀ (k : Fin units.size), ¬k = j1 → ¬k = j2 → ¬units[↑k].fst.val = ↑i
j1_lt_updatedUnits_size : ↑j1 < (insertUnit (units, assignments, foundContradiction) l).fst.size
j2_lt_updatedUnits_size : ↑j2 < (insertUnit (units, assignments, foundContradiction) l).fst.size
⊢ ∀
    (k :
      Fin
        (if hasAssignment l.snd assignments[l.fst.val]! = true then (units, assignments, foundContradiction)
            else
              (units.push (l.fst, l.snd), assignments.modify l.fst.val (addAssignment l.snd),
                foundContradiction || assignments[l.fst.val]! != unassigned)).fst.size),
    ¬k = ⟨↑j1, j1_lt_updatedUnits_size⟩ →
      ¬k = ⟨↑j2, j2_lt_updatedUnits_size⟩ →
        ¬(if hasAssignment l.snd assignments[l.fst.val]! = true then (units, assignments, foundContradiction)
                    else
                      (units.push l, assignments.modify l.fst.val (addAssignment l.snd),
                        foundContradiction || assignments[l.fst.val]! != unassigned)).fst[↑k].fst.val =
            ↑i
no goals