have hb : strong_assignments_invariant f := h.2
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
hb : f.strong_assignments_invariant
⊢ (List.foldl (fun f id => f.deleteOne id) f arr.data).strong_assignments_invariant