simp only [insert]
n : Nat
f : DefaultFormula n
c : DefaultClause n
f_readyForRupAdd : f.readyForRupAdd
⊢ (f.insert c).readyForRupAdd
n : Nat
f : DefaultFormula n
c : DefaultClause n
f_readyForRupAdd : f.readyForRupAdd
⊢ (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 }).readyForRupAdd