let motive := clear_insert_induction_motive f hf.2 (insertRatUnits f units).1.ratUnits
case assignments
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
⊢ 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
⊢ Array.foldl clearUnit (f.insertRatUnits units).1.assignments (f.insertRatUnits units).1.ratUnits 0 = f.assignments