tauto
case h
X : Finset Formula
ψ ϕ : Formula
psi_in_X : ψ ∈ X
sub_voc : ∀ ⦃x : Char⦄, x ∈ vocabOfFormula ϕ → x ∈ vocabOfFormula ψ
a : Char
h✝ : a ∈ vocabOfFormula ϕ
⊢ ψ ∈ X ∧ a ∈ vocabOfFormula ψ
no goals