exact not_in_S
X : Finset Formula
ϕ : Formula
S : Finset Formula
not_in_S : ϕ ∉ S
ih : S ⊆ X → lengthOfSet (X \ S) + lengthOfSet S = lengthOfSet X
h : insert ϕ S ⊆ X
subs_X : S ⊆ X
phi_in_X : ϕ ∈ X
⊢ ϕ ∉ S
no goals