next id_eq_idx =>
exfalso
have idx_in_bounds2 : idx.1 < f.clauses.size := by
  have f_clauses_rw : f.clauses = { data := f.clauses.data } := rfl
  conv => rhs; rw [f_clauses_rw, Array.size_mk]
  exact idx.2
simp only [getElem!, id_eq_idx, Array.data_length, idx_in_bounds2, ↓reduceDite,
  Fin.eta, Array.get_eq_getElem, Array.getElem_eq_data_get] at heq
rw [hidx, hl] at heq
simp only [unit, Option.some.injEq, DefaultClause.mk.injEq, List.cons.injEq, and_true] at heq
simp only [← heq, not] at l_ne_b
split at l_ne_b
. simp only at l_ne_b
. simp only at l_ne_b
case pos
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
l_eq_i : l.fst.val = i.val
hb✝ : hasAssignment b (removeAssignment (!b) f.assignments[i.val]) = true
l_ne_b : l.snd = !b
hb : hasAssignment b f.assignments[i.val] = true
hf : some (unit (i, b)) ∈ f.clauses.data
h✝¹ : id < f.clauses.size
idx : Fin f.clauses.data.length
hidx : f.clauses.data.get idx = some (unit (i, b))
idx_in_bounds : ↑idx < (f.clauses.data.set id none).length
h✝ : id = ↑idx
⊢ (f.clauses.data.set id none).get ⟨↑idx, idx_in_bounds⟩ = f.clauses.data.get idx
no goals