intro a aIn
X Y : Finset Formula
hyp : X ⊆ Y
⊢ ∀ x ∈ X, vocabOfFormula x ⊆ Y.biUnion vocabOfFormula
X Y : Finset Formula
hyp : X ⊆ Y
a : Formula
aIn : a ∈ X
⊢ vocabOfFormula a ⊆ Y.biUnion vocabOfFormula