unfold bigDis at hyp
case inr
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 inr
x : Char
head : Formula
tail : List Formula
ih : x ∈ voc (bigDis tail) → ∃ φ ∈ tail, x ∈ voc φ
h✝ : x ∉ vocabOfFormula head
hyp :
  x ∈
    voc
      (match head :: tail with
      | [] => ⊥
      | [f] => f
      | f :: rest => f⋁bigDis rest)
⊢ ∃ φ ∈ head :: tail, x ∈ voc φ