case insert ψ S _ _ =>
  intro psi_in_insert
  simp at *
  intro a aIn
  aesop
ϕ ψ : Formula
S : Finset Formula
a✝¹ : ψ ∉ S
a✝ : ϕ ∈ S → vocabOfFormula ϕ ⊆ vocabOfSetFormula S
⊢ ϕ ∈ insert ψ S → vocabOfFormula ϕ ⊆ vocabOfSetFormula (insert ψ S)
no goals