constructor
case h
X : Finset Formula
ψ ϕ1 ϕ2 : Formula
psi_in_X : ψ ∈ X
eq_voc : vocabOfFormula ϕ1 ∪ vocabOfFormula ϕ2 = vocabOfFormula ψ
a✝ : Char
h✝ : a✝ ∈ vocabOfFormula ϕ1 ∨ a✝ ∈ vocabOfFormula ϕ2
⊢ ψ ∈ X ∧ a✝ ∈ vocabOfFormula ψ
case h.left
X : Finset Formula
ψ ϕ1 ϕ2 : Formula
psi_in_X : ψ ∈ X
eq_voc : vocabOfFormula ϕ1 ∪ vocabOfFormula ϕ2 = vocabOfFormula ψ
a✝ : Char
h✝ : a✝ ∈ vocabOfFormula ϕ1 ∨ a✝ ∈ vocabOfFormula ϕ2
⊢ ψ ∈ X

case h.right
X : Finset Formula
ψ ϕ1 ϕ2 : Formula
psi_in_X : ψ ∈ X
eq_voc : vocabOfFormula ϕ1 ∪ vocabOfFormula ϕ2 = vocabOfFormula ψ
a✝ : Char
h✝ : a✝ ∈ vocabOfFormula ϕ1 ∨ a✝ ∈ vocabOfFormula ϕ2
⊢ a✝ ∈ vocabOfFormula ψ