simp
f✝ : Formula
S : Finset Formula
f_not_in_S : f✝ ∉ S
IH : lengthOfSet (projection S) ≤ lengthOfSet S
X : Finset Formula
f : Formula
⊢ (let X := insert f X;
    X.biUnion fun x => (formProjection x).toFinset) =
    (let X := {f};
      X.biUnion fun x => (formProjection x).toFinset) ∪
      let X := X;
      X.biUnion fun x => (formProjection x).toFinset
no goals