simp only [clearRatUnits]
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
⊢ (f.insertRatUnits units).fst.clearRatUnits = f
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
⊢ { clauses := (f.insertRatUnits units).1.clauses, rupUnits := (f.insertRatUnits units).1.rupUnits, ratUnits := #[],
      assignments :=
        Array.foldl clearUnit (f.insertRatUnits units).1.assignments (f.insertRatUnits units).1.ratUnits 0 } =
    f