intro X f
f : Formula
S : Finset Formula
f_not_in_S : f ∉ S
IH : lengthOfSet (projection S) ≤ lengthOfSet S
⊢ ∀ (X : Finset Formula) (f : Formula), projection (insert f X) = projection {f} ∪ projection X
f✝ : Formula
S : Finset Formula
f_not_in_S : f✝ ∉ S
IH : lengthOfSet (projection S) ≤ lengthOfSet S
X : Finset Formula
f : Formula
⊢ projection (insert f X) = projection {f} ∪ projection X