constructor
case a
X : Finset Formula
ψ ϕ : Formula
psi_in_X : ψ ∈ X
eq_voc : vocabOfFormula ϕ = vocabOfFormula ψ
a✝ : Char
⊢ a✝ ∈ X.biUnion vocabOfFormula ↔ a✝ ∈ vocabOfFormula ϕ ∪ (X.erase ψ).biUnion vocabOfFormula
case a.mp
X : Finset Formula
ψ ϕ : Formula
psi_in_X : ψ ∈ X
eq_voc : vocabOfFormula ϕ = vocabOfFormula ψ
a✝ : Char
⊢ 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✝ ∈ vocabOfFormula ϕ ∪ (X.erase ψ).biUnion vocabOfFormula → a✝ ∈ X.biUnion vocabOfFormula