constructor
case a
X : Finset Formula
ψ ϕ1 ϕ2 : Formula
psi_in_X : ψ ∈ X
eq_voc : vocabOfFormula ϕ1 ∪ vocabOfFormula ϕ2 = vocabOfFormula ψ
a✝ : Char
⊢ a✝ ∈ X.biUnion vocabOfFormula ↔ a✝ ∈ (X.erase ψ).biUnion vocabOfFormula ∪ (vocabOfFormula ϕ1 ∪ vocabOfFormula ϕ2)
case a.mp
X : Finset Formula
ψ ϕ1 ϕ2 : Formula
psi_in_X : ψ ∈ X
eq_voc : vocabOfFormula ϕ1 ∪ vocabOfFormula ϕ2 = vocabOfFormula ψ
a✝ : Char
⊢ a✝ ∈ X.biUnion vocabOfFormula → a✝ ∈ (X.erase ψ).biUnion vocabOfFormula ∪ (vocabOfFormula ϕ1 ∪ vocabOfFormula ϕ2)

case a.mpr
X : Finset Formula
ψ ϕ1 ϕ2 : Formula
psi_in_X : ψ ∈ X
eq_voc : vocabOfFormula ϕ1 ∪ vocabOfFormula ϕ2 = vocabOfFormula ψ
a✝ : Char
⊢ a✝ ∈ (X.erase ψ).biUnion vocabOfFormula ∪ (vocabOfFormula ϕ1 ∪ vocabOfFormula ϕ2) → a✝ ∈ X.biUnion vocabOfFormula