all_goals intro a_in
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
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