simp only [insert]
n : Nat
f : DefaultFormula n
c : DefaultClause n
⊢ (f.insert c).assignments.size = f.assignments.size
n : Nat
f : DefaultFormula n
c : DefaultClause n
⊢ (match c.isUnit with
        | none =>
          { clauses := f.clauses.push (some c), rupUnits := f.rupUnits, ratUnits := f.ratUnits,
            assignments := f.assignments }
        | some (l, true) =>
          { clauses := f.clauses.push (some c), rupUnits := f.rupUnits, ratUnits := f.ratUnits,
            assignments := f.assignments.modify l.val addPosAssignment }
        | some (l, false) =>
          { clauses := f.clauses.push (some c), rupUnits := f.rupUnits, ratUnits := f.ratUnits,
            assignments := f.assignments.modify l.val addNegAssignment }).assignments.size =
    f.assignments.size