induction l
x : Char
l : List Formula
hyp : x ∈ voc (bigDis l)
⊢ ∃ φ ∈ l, x ∈ voc φ
case nil
x : Char
hyp : x ∈ voc (bigDis [])
⊢ ∃ φ ∈ [], x ∈ voc φ

case cons
x : Char
head✝ : Formula
tail✝ : List Formula
tail_ih✝ : x ∈ voc (bigDis tail✝) → ∃ φ ∈ tail✝, x ∈ voc φ
hyp : x ∈ voc (bigDis (head✝ :: tail✝))
⊢ ∃ φ ∈ head✝ :: tail✝, x ∈ voc φ