intro p pIn
X Y : Finset Formula
hyp : X ⊆ Y
a : Formula
aIn : a ∈ X
⊢ vocabOfFormula a ⊆ (Y.val.bind fun a => (vocabOfFormula a).val).toFinset
X Y : Finset Formula
hyp : X ⊆ Y
a : Formula
aIn : a ∈ X
p : Char
pIn : p ∈ vocabOfFormula a
⊢ p ∈ (Y.val.bind fun a => (vocabOfFormula a).val).toFinset