intro φ φ_in_proj ℓ ℓ_in_φ
X : Finset Formula
⊢ ∀ x ∈ projection X, vocabOfFormula x ⊆ X.biUnion vocabOfFormula
X : Finset Formula
φ : Formula
φ_in_proj : φ ∈ projection X
ℓ : Char
ℓ_in_φ : ℓ ∈ vocabOfFormula φ
⊢ ℓ ∈ X.biUnion vocabOfFormula