simp at a_in_vocTheta
case pos.h
X : Finset Formula
ϕ1 ϕ2 : Formula
a✝ : Char
θ : Formula
theta_in_X psi_in_X : θ ∈ X
eq_voc :
  ((match ϕ1 with
      | Formula.bottom => ∅
      | ·c => {c}
      | ~φ => vocabOfFormula φ
      | φ⋀ψ => vocabOfFormula φ ∪ vocabOfFormula ψ
      | □φ => vocabOfFormula φ) ∪
      match ϕ2 with
      | Formula.bottom => ∅
      | ·c => {c}
      | ~φ => vocabOfFormula φ
      | φ⋀ψ => vocabOfFormula φ ∪ vocabOfFormula ψ
      | □φ => vocabOfFormula φ) =
    match θ with
    | Formula.bottom => ∅
    | ·c => {c}
    | ~φ => vocabOfFormula φ
    | φ⋀ψ => vocabOfFormula φ ∪ vocabOfFormula ψ
    | □φ => vocabOfFormula φ
a_in_vocTheta :
  a✝ ∈
    (match ϕ1 with
      | Formula.bottom => ∅
      | ·c => {c}
      | ~φ => vocabOfFormula φ
      | φ⋀ψ => vocabOfFormula φ ∪ vocabOfFormula ψ
      | □φ => vocabOfFormula φ) ∪
      match ϕ2 with
      | Formula.bottom => ∅
      | ·c => {c}
      | ~φ => vocabOfFormula φ
      | φ⋀ψ => vocabOfFormula φ ∪ vocabOfFormula ψ
      | □φ => vocabOfFormula φ
⊢ (a✝ ∈
      match ϕ1 with
      | Formula.bottom => ∅
      | ·c => {c}
      | ~φ => vocabOfFormula φ
      | φ⋀ψ => vocabOfFormula φ ∪ vocabOfFormula ψ
      | □φ => vocabOfFormula φ) ∨
    a✝ ∈
      match ϕ2 with
      | Formula.bottom => ∅
      | ·c => {c}
      | ~φ => vocabOfFormula φ
      | φ⋀ψ => vocabOfFormula φ ∪ vocabOfFormula ψ
      | □φ => vocabOfFormula φ
case pos.h
X : Finset Formula
ϕ1 ϕ2 : Formula
a✝ : Char
θ : Formula
theta_in_X psi_in_X : θ ∈ X
eq_voc :
  ((match ϕ1 with
      | Formula.bottom => ∅
      | ·c => {c}
      | ~φ => vocabOfFormula φ
      | φ⋀ψ => vocabOfFormula φ ∪ vocabOfFormula ψ
      | □φ => vocabOfFormula φ) ∪
      match ϕ2 with
      | Formula.bottom => ∅
      | ·c => {c}
      | ~φ => vocabOfFormula φ
      | φ⋀ψ => vocabOfFormula φ ∪ vocabOfFormula ψ
      | □φ => vocabOfFormula φ) =
    match θ with
    | Formula.bottom => ∅
    | ·c => {c}
    | ~φ => vocabOfFormula φ
    | φ⋀ψ => vocabOfFormula φ ∪ vocabOfFormula ψ
    | □φ => vocabOfFormula φ
a_in_vocTheta :
  (a✝ ∈
      match ϕ1 with
      | Formula.bottom => ∅
      | ·c => {c}
      | ~φ => vocabOfFormula φ
      | φ⋀ψ => vocabOfFormula φ ∪ vocabOfFormula ψ
      | □φ => vocabOfFormula φ) ∨
    a✝ ∈
      match ϕ2 with
      | Formula.bottom => ∅
      | ·c => {c}
      | ~φ => vocabOfFormula φ
      | φ⋀ψ => vocabOfFormula φ ∪ vocabOfFormula ψ
      | □φ => vocabOfFormula φ
⊢ (a✝ ∈
      match ϕ1 with
      | Formula.bottom => ∅
      | ·c => {c}
      | ~φ => vocabOfFormula φ
      | φ⋀ψ => vocabOfFormula φ ∪ vocabOfFormula ψ
      | □φ => vocabOfFormula φ) ∨
    a✝ ∈
      match ϕ2 with
      | Formula.bottom => ∅
      | ·c => {c}
      | ~φ => vocabOfFormula φ
      | φ⋀ψ => vocabOfFormula φ ∪ vocabOfFormula ψ
      | □φ => vocabOfFormula φ