Theorem: inVocList (Pdl/Vocab.lean)

State before:
ℓ : ℕ
L : List Formula
⊢ ℓ ∈ vocabOfListFormula L ↔ ∃ φ ∈ L, ℓ ∈ vocabOfFormula φ
Tactic:
simp only [vocabOfListFormula, Finset.mem_biUnion, List.mem_toFinset]
State after:
no goals