have li_in_derivedLits : li ∈ derivedLits := by
  have derivedLits_rw : derivedLits = (Array.mk derivedLits).data := by simp only
  simp only [derivedLits_arr_def, li]
  conv => rhs; rw [derivedLits_rw]
  apply Array.getElem_mem_data
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
f'_assignments_size : (f.performRupCheck rupHints).fst.assignments.size = n
derivedLits : List (Literal (PosFin n))
derivedLits_satisfies_invariant :
  f.derivedLits_invariant f_assignments_size (f.performRupCheck rupHints).fst.assignments f'_assignments_size
    derivedLits
derivedLits_arr : Array (Literal (PosFin n))
derivedLits_arr_def : derivedLits_arr = { data := derivedLits }
i j : Fin derivedLits_arr.size
i_ne_j : i ≠ j
li_eq_lj : derivedLits_arr[i] = derivedLits_arr[j]
li : Literal (PosFin n) := derivedLits_arr[i]
⊢ False
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
f'_assignments_size : (f.performRupCheck rupHints).fst.assignments.size = n
derivedLits : List (Literal (PosFin n))
derivedLits_satisfies_invariant :
  f.derivedLits_invariant f_assignments_size (f.performRupCheck rupHints).fst.assignments f'_assignments_size
    derivedLits
derivedLits_arr : Array (Literal (PosFin n))
derivedLits_arr_def : derivedLits_arr = { data := derivedLits }
i j : Fin derivedLits_arr.size
i_ne_j : i ≠ j
li_eq_lj : derivedLits_arr[i] = derivedLits_arr[j]
li : Literal (PosFin n) := derivedLits_arr[i]
li_in_derivedLits : li ∈ derivedLits
⊢ False