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