rw [deleteOne_preserves_rupUnits, ih]
n : Nat
f : DefaultFormula n
arr : Array Nat
h : f.readyForRupAdd
hb : f.rupUnits = #[]
acc : DefaultFormula n
ih : acc.rupUnits = #[]
id : Nat
_id_in_arr : id ∈ arr.data
⊢ (acc.deleteOne id).rupUnits = #[]
no goals