apply lengthAdd
X : Finset Formula
ϕ : Formula
in_X : ϕ ∈ X
⊢ lengthOfSet (insert ϕ (X \ {ϕ})) = lengthOfSet (X \ {ϕ}) + lengthOfFormula ϕ
case a
X : Finset Formula
ϕ : Formula
in_X : ϕ ∈ X
⊢ ϕ ∉ X \ {ϕ}