have h_base : motive 0 (insertRupUnits f units).1.assignments := clear_insertRup_base_case f f_readyForRupAdd units
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
⊢ 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
⊢ Array.foldl clearUnit (f.insertRupUnits units).1.assignments (f.insertRupUnits units).1.rupUnits 0 = f.assignments