all_goals norm_num at *
case a.mp
X : Finset Formula
ψ ϕ : Formula
psi_in_X : ψ ∈ X
eq_voc : vocabOfFormula ϕ = vocabOfFormula ψ
a✝ : Char
a_in : a✝ ∈ X.biUnion vocabOfFormula
⊢ a✝ ∈ vocabOfFormula ϕ ∪ (X.erase ψ).biUnion vocabOfFormula

case a.mpr
X : Finset Formula
ψ ϕ : Formula
psi_in_X : ψ ∈ X
eq_voc : vocabOfFormula ϕ = vocabOfFormula ψ
a✝ : Char
a_in : a✝ ∈ vocabOfFormula ϕ ∪ (X.erase ψ).biUnion vocabOfFormula
⊢ a✝ ∈ X.biUnion vocabOfFormula
case a.mp
X : Finset Formula
ψ ϕ : Formula
psi_in_X : ψ ∈ X
eq_voc : vocabOfFormula ϕ = vocabOfFormula ψ
a✝ : Char
a_in : ∃ a ∈ X, a✝ ∈ vocabOfFormula a
⊢ a✝ ∈ vocabOfFormula ϕ ∨ ∃ a, (¬a = ψ ∧ a ∈ X) ∧ a✝ ∈ vocabOfFormula a

case a.mpr
X : Finset Formula
ψ ϕ : Formula
psi_in_X : ψ ∈ X
eq_voc : vocabOfFormula ϕ = vocabOfFormula ψ
a✝ : Char
a_in : a✝ ∈ vocabOfFormula ϕ ∨ ∃ a, (¬a = ψ ∧ a ∈ X) ∧ a✝ ∈ vocabOfFormula a
⊢ ∃ a ∈ X, a✝ ∈ vocabOfFormula a