intro ϕ in_X
X : Finset Formula
⊢ ∀ ϕ ∈ X, lengthOfSet (X.erase ϕ) + lengthOfFormula ϕ = lengthOfSet X
X : Finset Formula
ϕ : Formula
in_X : ϕ ∈ X
⊢ lengthOfSet (X.erase ϕ) + lengthOfFormula ϕ = lengthOfSet X