next bi_eq_false =>
simp only [Bool.not_eq_true] at bi_eq_false
by_cases i = k2
. next i_eq_k2 =>
  have j_ne_k2 : j ≠ k2 := by rw [← i_eq_k2]; exact i_ne_j.symm
  by_cases j = k1
  . next j_eq_k1 =>
    rw [← j_eq_k1, hj, ← bi_eq_bj, bi_eq_false] at h1
    simp only [Prod.mk.injEq, and_false] at h1
  . next j_ne_k1 =>
    specialize h5 j j_ne_k1 j_ne_k2
    rw [hj, li_eq_lj] at h5
    simp (config := { decide := true}) only at h5
. next i_ne_k2 =>
  by_cases i = k1
  . next i_eq_k1 =>
    rw [← i_eq_k1, hi, bi_eq_false] at h1
    simp only [Prod.mk.injEq, and_false] at h1
  . next i_ne_k1 =>
    specialize h5 i i_ne_k1 i_ne_k2
    rw [hi] at h5
    simp only [not_true] at h5
case neg
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
units : List (Literal (PosFin n))
i j : Fin (f.insertRupUnits units).fst.rupUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRupUnits units).fst.rupUnits[i] = (li, bi)
lj : PosFin n
bj : Bool
hj : (f.insertRupUnits units).fst.rupUnits[j] = (lj, bj)
li_eq_lj : li = lj
bi_eq_bj : bi = bj
k1 k2 : Fin (f.insertRupUnits units).fst.rupUnits.size
li_gt_zero : li.val > 0
h1 : (f.insertRupUnits units).fst.rupUnits[k1] = (⟨li.val, ⋯⟩, true)
h2 : (f.insertRupUnits units).fst.rupUnits[k2] = (⟨li.val, ⋯⟩, false)
h3 : (f.insertRupUnits units).fst.assignments[li.val] = both
h4 : f.assignments[li.val] = unassigned
h5 :
  ∀ (k : Fin (f.insertRupUnits units).fst.rupUnits.size),
    ¬k = k1 → ¬k = k2 → ¬(f.insertRupUnits units).fst.rupUnits[k].fst.val = li.val
h✝ : ¬bi = true
⊢ False
no goals