induction X using Finset.induction_on
ϕ : Formula
X : Finset Formula
⊢ ϕ ∈ X → vocabOfFormula ϕ ⊆ vocabOfSetFormula X
case empty
ϕ : Formula
⊢ ϕ ∈ ∅ → vocabOfFormula ϕ ⊆ vocabOfSetFormula ∅

case insert
ϕ a✝² : Formula
s✝ : Finset Formula
a✝¹ : a✝² ∉ s✝
a✝ : ϕ ∈ s✝ → vocabOfFormula ϕ ⊆ vocabOfSetFormula s✝
⊢ ϕ ∈ insert a✝² s✝ → vocabOfFormula ϕ ⊆ vocabOfSetFormula (insert a✝² s✝)