. rcases List.get_of_mem hf with ⟨idx, hidx⟩
  simp only [← hidx, Array.data_set]
  rw [List.mem_iff_get]
  have idx_in_bounds : idx.1 < List.length (List.set f.clauses.data id none) := by
    simp only [List.length_set]
    exact idx.2
  apply Exists.intro ⟨idx.1, idx_in_bounds⟩
  by_cases id = idx
  . 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
    have i_eq_l : i = l.1 := by rw [← heq]
    simp only [i_eq_l, not_true] at l_ne_i
  . next id_ne_idx =>
    simp only [ne_eq, id_ne_idx, not_false_eq_true, List.get_set_ne]
case inl.h.isTrue
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_ne_i : ¬l.fst.val = i.val
l_in_bounds : l.fst.val < f.assignments.size
hb : hasAssignment b f.assignments[i.val] = true
hf : some (unit (i, b)) ∈ f.clauses.data
h✝ : id < f.clauses.size
⊢ some (unit (i, b)) ∈ (f.clauses.set ⟨id, h✝⟩ none).data

case inl.h.isFalse
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_ne_i : ¬l.fst.val = i.val
l_in_bounds : l.fst.val < f.assignments.size
hb : hasAssignment b f.assignments[i.val] = true
hf : some (unit (i, b)) ∈ f.clauses.data
h✝ : ¬id < f.clauses.size
⊢ some (unit (i, b)) ∈ f.clauses.data
case inl.h.isFalse
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_ne_i : ¬l.fst.val = i.val
l_in_bounds : l.fst.val < f.assignments.size
hb : hasAssignment b f.assignments[i.val] = true
hf : some (unit (i, b)) ∈ f.clauses.data
h✝ : ¬id < f.clauses.size
⊢ some (unit (i, b)) ∈ f.clauses.data