intro a aInVocPhi
X : Finset Formula
ϕ : Formula
phi_in_proj : □ϕ ∈ X
⊢ vocabOfFormula ϕ ⊆ X.biUnion vocabOfFormula
X : Finset Formula
ϕ : Formula
phi_in_proj : □ϕ ∈ X
a : Char
aInVocPhi : a ∈ vocabOfFormula ϕ
⊢ a ∈ X.biUnion vocabOfFormula