rw [proj] at φ_in_proj
X : Finset Formula
φ : Formula
φ_in_proj : φ ∈ projection X
ℓ : Char
ℓ_in_φ : ℓ ∈ vocabOfFormula φ
⊢ ℓ ∈ X.biUnion vocabOfFormula
X : Finset Formula
φ : Formula
φ_in_proj : □φ ∈ X
ℓ : Char
ℓ_in_φ : ℓ ∈ vocabOfFormula φ
⊢ ℓ ∈ X.biUnion vocabOfFormula