tauto
case inl
x : Char
head : Formula
tail : List Formula
ih : x ∈ voc (bigCon tail) → ∃ φ ∈ tail, x ∈ voc φ
hyp : x ∈ voc (bigCon (head :: tail))
h✝ : x ∈ vocabOfFormula head
⊢ x ∈ vocabOfFormula head ∨ ∃ a ∈ tail, x ∈ vocabOfFormula a
no goals