next l _ _ heq =>
simp only [Option.some.injEq] at heq
rw [heq] at hl
specialize hl l.1
simp only [DefaultClause.mk.injEq, List.cons.injEq, and_true] at hl
by_cases hl2 : l.2
. simp only [← hl2, Prod.mk.eta, not_true, and_false] at hl
. simp only [Bool.not_eq_true] at hl2
  simp only [← hl2, Prod.mk.eta, not_true, false_and] at hl
case neg.h_2
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hf : ∀ (i : PosFin n) (b : Bool), hasAssignment b f.assignments[i.val] = true → unit (i, b) ∈ f.toList
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
hb : hasAssignment b (f.deleteOne id).assignments[i.val] = true
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
hl :
  ∀ (x : PosFin n),
    ¬c = { clause := [(x, false)], nodupkey := ⋯, nodup := ⋯ } ∧
      ¬c = { clause := [(x, true)], nodupkey := ⋯, nodup := ⋯ }
x✝ : Option (DefaultClause n)
l✝ : Literal (PosFin n)
nodupkey✝ : ∀ (l : PosFin n), ¬(l, true) ∈ [l✝] ∨ ¬(l, false) ∈ [l✝]
nodup✝ : [l✝].Nodup
heq✝ : some c = some { clause := [l✝], nodupkey := nodupkey✝, nodup := nodup✝ }
⊢ unit (i, b) ∈
    { clauses := f.clauses.set! id none, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
        assignments := f.assignments.modify l✝.fst.val (removeAssignment l✝.snd) }.toList
no goals