rcases hl with ⟨l, hl⟩
case pos
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 : ∃ l, c = unit l
⊢ unit (i, b) ∈
    (match some c with
      | none => { clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits, assignments := f.assignments }
      | some { clause := [l], nodupkey := nodupkey, nodup := nodup } =>
        { clauses := f.clauses.set! id none, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
          assignments := f.assignments.modify l.fst.val (removeAssignment l.snd) }
      | some val =>
        { clauses := f.clauses.set! id none, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
          assignments := f.assignments }).toList
case pos.intro
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
l : Literal (PosFin n)
hl : c = unit l
⊢ unit (i, b) ∈
    (match some c with
      | none => { clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits, assignments := f.assignments }
      | some { clause := [l], nodupkey := nodupkey, nodup := nodup } =>
        { clauses := f.clauses.set! id none, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
          assignments := f.assignments.modify l.fst.val (removeAssignment l.snd) }
      | some val =>
        { clauses := f.clauses.set! id none, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
          assignments := f.assignments }).toList