simp
g : Formula
X : Finset Formula
⊢ (g ∈
      let X := X;
      X.biUnion fun x => (formProjection x).toFinset) ↔
    □g ∈ X
g : Formula
X : Finset Formula
⊢ (∃ a ∈ X,
      (match a with
        | □f => some f
        | x => none) =
        some g) ↔
    □g ∈ X