. have hb : strong_assignments_invariant f := h.2
  have hl (acc : DefaultFormula n) (ih : strong_assignments_invariant acc) (id : Nat) (_id_in_arr : id ∈ arr.data) :
    strong_assignments_invariant (deleteOne acc id) := deleteOne_preserves_strong_assignments_invariant acc id ih
  exact List.foldlRecOn arr.data deleteOne f hb hl
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
no goals