. simp only [insertRatUnits]
case rupUnits
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 }.rupUnits =
    f.rupUnits

case ratUnits
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 }.ratUnits =
    f.ratUnits

case assignments
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 }.assignments =
    f.assignments
case ratUnits
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 }.ratUnits =
    f.ratUnits

case assignments
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 }.assignments =
    f.assignments