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