simp only [delete, Array.foldl_eq_foldl_data]
n : Nat
f : DefaultFormula n
arr : Array Nat
c : DefaultClause n
⊢ c ∈ (f.delete arr).toList → c ∈ f.toList
n : Nat
f : DefaultFormula n
arr : Array Nat
c : DefaultClause n
⊢ c ∈ (List.foldl (fun f id => f.deleteOne id) f arr.data).toList → c ∈ f.toList