rw [proj] at phi_in_proj
X : Finset Formula
ϕ : Formula
phi_in_proj : ϕ ∈ projection X
⊢ vocabOfFormula ϕ ⊆ X.biUnion vocabOfFormula
X : Finset Formula
ϕ : Formula
phi_in_proj : □ϕ ∈ X
⊢ vocabOfFormula ϕ ⊆ X.biUnion vocabOfFormula