simp only [deleteOne]
n : Nat
f : DefaultFormula n
id : Nat
c : DefaultClause n
⊢ c ∈ (f.deleteOne id).toList → c ∈ f.toList
n : Nat
f : DefaultFormula n
id : Nat
c : DefaultClause n
⊢ c ∈
      (match f.clauses[id]! 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 →
    c ∈ f.toList