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
case assignments
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
units : List (Literal (PosFin n))
motive : Nat → Array Assignment → Prop := f.clear_insert_induction_motive ⋯ (f.insertRupUnits units).fst.rupUnits
h_base : motive 0 (f.insertRupUnits units).fst.assignments
⊢ Array.foldl clearUnit (f.insertRupUnits units).1.assignments (f.insertRupUnits units).1.rupUnits 0 = f.assignments
case assignments
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
units : List (Literal (PosFin n))
motive : Nat → Array Assignment → Prop := f.clear_insert_induction_motive ⋯ (f.insertRupUnits units).fst.rupUnits
h_base : motive 0 (f.insertRupUnits units).fst.assignments
h_inductive :
  ∀ (idx : Fin (f.insertRupUnits units).fst.rupUnits.size) (assignments : Array Assignment),
    motive (↑idx) assignments → motive (↑idx + 1) (clearUnit assignments (f.insertRupUnits units).fst.rupUnits[idx])
⊢ Array.foldl clearUnit (f.insertRupUnits units).1.assignments (f.insertRupUnits units).1.rupUnits 0 = f.assignments