rw [f_readyForRupAdd.2.1] at insertRupUnits_assignments_size
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
units : List (Literal (PosFin n))
insertRupUnits_assignments_size : (f.insertRupUnits units).fst.assignments.size = f.assignments.size
⊢ f.clear_insert_induction_motive ⋯ (f.insertRupUnits units).fst.rupUnits 0 (f.insertRupUnits units).fst.assignments
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
units : List (Literal (PosFin n))
insertRupUnits_assignments_size : (f.insertRupUnits units).fst.assignments.size = n
⊢ f.clear_insert_induction_motive ⋯ (f.insertRupUnits units).fst.rupUnits 0 (f.insertRupUnits units).fst.assignments