have rupAddSuccess : DefaultFormula.insert (clearRupUnits (insertRupUnits f (negate c)).fst) c = f' := by
  rw [rupAddSuccess]
case isFalse.isFalse.isFalse
n : Nat
f : DefaultFormula n
c : DefaultClause n
rupHints : Array Nat
f' : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
h✝² : ¬(f.insertRupUnits c.negate).snd = true
h✝¹ : ¬((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.snd = true
h✝ : ¬((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.fst = false
fc : DefaultFormula n := (f.insertRupUnits c.negate).fst
fc_assignments_size : (f.insertRupUnits c.negate).fst.assignments.size = n
rupAddSuccess :
  { clauses := (f.insertRupUnits c.negate).fst.clauses, rupUnits := (f.insertRupUnits c.negate).fst.rupUnits,
            ratUnits := (f.insertRupUnits c.negate).fst.ratUnits, assignments := fc.assignments }.clearRupUnits.insert
      c =
    f'
⊢ f' = f.insert c
case isFalse.isFalse.isFalse
n : Nat
f : DefaultFormula n
c : DefaultClause n
rupHints : Array Nat
f' : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
h✝² : ¬(f.insertRupUnits c.negate).snd = true
h✝¹ : ¬((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.snd = true
h✝ : ¬((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.fst = false
fc : DefaultFormula n := (f.insertRupUnits c.negate).fst
fc_assignments_size : (f.insertRupUnits c.negate).fst.assignments.size = n
rupAddSuccess✝ :
  { clauses := (f.insertRupUnits c.negate).fst.clauses, rupUnits := (f.insertRupUnits c.negate).fst.rupUnits,
            ratUnits := (f.insertRupUnits c.negate).fst.ratUnits, assignments := fc.assignments }.clearRupUnits.insert
      c =
    f'
rupAddSuccess : (f.insertRupUnits c.negate).fst.clearRupUnits.insert c = f'
⊢ f' = f.insert c