exact List.foldlRecOn arr.data deleteOne f hb hl
case right
n : Nat
f : DefaultFormula n
arr : Array Nat
h : f.readyForRupAdd
hb : f.strong_assignments_invariant
hl :
  ∀ (acc : DefaultFormula n),
    acc.strong_assignments_invariant → ∀ (id : Nat), id ∈ arr.data → (acc.deleteOne id).strong_assignments_invariant
⊢ (List.foldl (fun f id => f.deleteOne id) f arr.data).strong_assignments_invariant
no goals