unfold Finset.biUnion at *
X Y : Finset Formula
hyp : X ⊆ Y
a : Formula
aIn : a ∈ X
⊢ vocabOfFormula a ⊆ Y.biUnion vocabOfFormula
X Y : Finset Formula
hyp : X ⊆ Y
a : Formula
aIn : a ∈ X
⊢ vocabOfFormula a ⊆ (Y.val.bind fun a => (vocabOfFormula a).val).toFinset