. have hb : f.rupUnits = #[] := h.1
  have hl (acc : DefaultFormula n) (ih : acc.rupUnits = #[]) (id : Nat) (_id_in_arr : id ∈ arr.data) :
    (deleteOne acc id).rupUnits = #[] := by rw [deleteOne_preserves_rupUnits, ih]
  exact List.foldlRecOn arr.data deleteOne f hb hl
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 right
n : Nat
f : DefaultFormula n
arr : Array Nat
h : f.readyForRupAdd
⊢ (List.foldl (fun f id => f.deleteOne id) f arr.data).strong_assignments_invariant
case right
n : Nat
f : DefaultFormula n
arr : Array Nat
h : f.readyForRupAdd
⊢ (List.foldl (fun f id => f.deleteOne id) f arr.data).strong_assignments_invariant