. simp only
  let motive := clear_insert_induction_motive f hf.2 (insertRatUnits f units).1.ratUnits
  have h_base : motive 0 (insertRatUnits f units).1.assignments := clear_insertRat_base_case f hf units
  have h_inductive (idx : Fin (insertRatUnits f units).1.ratUnits.size) (assignments : Array Assignment)
    (ih : motive idx.val assignments) : motive (idx.val + 1) (clearUnit assignments (insertRatUnits f units).1.ratUnits[idx]) :=
    clear_insert_inductive_case f hf.2 (insertRatUnits f units).1.ratUnits
      (insertRatUnits_nodup f hf units) idx assignments ih
  rcases Array.foldl_induction motive h_base h_inductive with ⟨h_size, h⟩
  apply Array.ext
  . rw [h_size, hf.2]
  . intro i hi1 hi2
    have i_lt_n : i < n := by omega
    specialize h ⟨i, i_lt_n⟩
    rcases h with h | h | h
    . exact h.1
    . omega
    . omega
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
no goals