simp only [insert_iff, Array.toList_eq, Array.data_toArray, List.mem_singleton]
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝¹ : Clause α β
inst✝ : Formula α β σ
c : β
f : σ
p : α → Bool
h : ∀ (x : β), x ∈ toList (insert f c) → p ⊨ x
c' : β
c'_in_f : c' ∈ toList f
⊢ c' ∈ toList (insert f c)
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝¹ : Clause α β
inst✝ : Formula α β σ
c : β
f : σ
p : α → Bool
h : ∀ (x : β), x ∈ toList (insert f c) → p ⊨ x
c' : β
c'_in_f : c' ∈ toList f
⊢ c' = c ∨ c' ∈ toList f