aesop
X Y : Finset Formula
⊢ (let X := X ∪ Y;
    X.biUnion fun x => (formProjection x).toFinset) =
    (let X := X;
      X.biUnion fun x => (formProjection x).toFinset) ∪
      let X := Y;
      X.biUnion fun x => (formProjection x).toFinset
no goals