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
f' : DefaultFormula n
ih : c ∈ f'.toList → c ∈ f.toList
id : Nat
x✝ : id ∈ arr.data
h : c ∈ (f'.deleteOne id).toList
⊢ c ∈ f.toList
no goals