. constructor
  . simp only [getElem!, l_in_bounds, ↓reduceDite, Array.get_eq_getElem,
    Bool.not_eq_true] at h3
    simp only [← i_eq_l, ← h1]
    simp only [i_eq_l, h3]
  . intro k hk
    have k_in_bounds : k.1 < units.size := by
      apply Nat.lt_of_le_of_ne
      . apply Nat.le_of_lt_succ
        have k_property := k.2
        simp only [insertUnit, h3, Prod.mk.eta, ite_false, Array.size_push] at k_property
        exact k_property
      . intro h
        simp only [← h, not_true, mostRecentUnitIdx] at hk
        exact hk rfl
    rw [Array.get_push_lt _ _ _ k_in_bounds]
    rw [i_eq_l] at h2
    exact h2 ⟨k.1, k_in_bounds⟩
case 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
h1 : assignments[↑i] = assignments0[↑i]
h2 : ∀ (j : Fin units.size), ¬units[↑j].fst.val = ↑i
h3 : ¬hasAssignment l.snd assignments[l.fst.val]! = true
i_eq_l : ↑i = l.fst.val
units_size_lt_updatedUnits_size : units.size < (insertUnit (units, assignments, foundContradiction) l).fst.size
mostRecentUnitIdx : Fin (insertUnit (units, assignments, foundContradiction) l).fst.size :=
  ⟨units.size, units_size_lt_updatedUnits_size⟩
i_gt_zero : ↑i > 0
⊢ hasAssignment l.snd assignments0[l.fst.val] = false ∧
    ∀
      (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 = mostRecentUnitIdx → ¬(units.push l)[↑k].fst.val = l.fst.val
no goals