. rw [delete, Array.foldl_eq_foldl_data]
  have hb : f.ratUnits = #[] := h.1
  have hl (acc : DefaultFormula n) (ih : acc.ratUnits = #[]) (id : Nat) (_id_in_arr : id ∈ arr.data) :
    (deleteOne acc id).ratUnits = #[] := by rw [deleteOne_preserves_ratUnits, ih]
  exact List.foldlRecOn arr.data deleteOne f hb hl
case left
n : Nat
f : DefaultFormula n
arr : Array Nat
h : f.readyForRatAdd
⊢ (f.delete arr).ratUnits = #[]

case right
n : Nat
f : DefaultFormula n
arr : Array Nat
h : f.readyForRatAdd
⊢ (f.delete arr).readyForRupAdd
case right
n : Nat
f : DefaultFormula n
arr : Array Nat
h : f.readyForRatAdd
⊢ (f.delete arr).readyForRupAdd