. simp only
  let motive := clear_insert_induction_motive f f_readyForRupAdd.2.1 (insertRupUnits f units).1.rupUnits
  have h_base : motive 0 (insertRupUnits f units).1.assignments := clear_insertRup_base_case f f_readyForRupAdd units
  have h_inductive (idx : Fin (insertRupUnits f units).1.rupUnits.size) (assignments : Array Assignment)
    (ih : motive idx.val assignments) : motive (idx.val + 1) (clearUnit assignments (insertRupUnits f units).1.rupUnits[idx]) :=
    clear_insert_inductive_case f f_readyForRupAdd.2.1 (insertRupUnits f units).1.rupUnits
      (insertRupUnits_nodup f f_readyForRupAdd units) idx assignments ih
  rcases Array.foldl_induction motive h_base h_inductive with ⟨h_size, h⟩
  apply Array.ext
  . rw [h_size, f_readyForRupAdd.2.1]
  . intro i hi1 hi2
    have i_lt_n : i < n := by rw [← f_readyForRupAdd.2.1]; exact hi2
    specialize h ⟨i, i_lt_n⟩
    rcases h with ⟨h,_⟩
    . exact h
    . omega
case assignments
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
units : List (Literal (PosFin n))
⊢ { clauses := (f.insertRupUnits units).1.clauses, rupUnits := #[], ratUnits := (f.insertRupUnits units).1.ratUnits,
        assignments :=
          Array.foldl clearUnit (f.insertRupUnits units).1.assignments (f.insertRupUnits units).1.rupUnits
            0 }.assignments =
    f.assignments
no goals