have hl (f' : DefaultFormula n) (ih : c ∈ toList f' → c ∈ toList f) (id : Nat) (_ : id ∈ arr.data) :
  c ∈ toList (deleteOne f' id) → c ∈ toList f := by intro h; exact ih $ deleteOne_subset f' id c h
n : Nat
f : DefaultFormula n
arr : Array Nat
c : DefaultClause n
hb : c ∈ f.toList → c ∈ f.toList
⊢ c ∈ (List.foldl (fun f id => f.deleteOne id) f arr.data).toList → c ∈ f.toList
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