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