have hb : f.rupUnits = #[] := h.1
case left
n : Nat
f : DefaultFormula n
arr : Array Nat
h : f.readyForRupAdd
⊢ (List.foldl (fun f id => f.deleteOne id) f arr.data).rupUnits = #[]
case left
n : Nat
f : DefaultFormula n
arr : Array Nat
h : f.readyForRupAdd
hb : f.rupUnits = #[]
⊢ (List.foldl (fun f id => f.deleteOne id) f arr.data).rupUnits = #[]