exact List.foldlRecOn arr.data deleteOne f hb hl
n : Nat
f : DefaultFormula n
arr : Array Nat
c : DefaultClause n
hb : c ∈ f.toList → c ∈ f.toList
hl :
  ∀ (f' : DefaultFormula n),
    (c ∈ f'.toList → c ∈ f.toList) → ∀ (id : Nat), id ∈ arr.data → c ∈ (f'.deleteOne id).toList → c ∈ f.toList
⊢ c ∈ (List.foldl (fun f id => f.deleteOne id) f arr.data).toList → c ∈ f.toList
no goals