intro notin
X : Finset Formula
ϕ : Formula
⊢ ϕ ∉ X → lengthOfSet (insert ϕ X) = lengthOfSet X + lengthOfFormula ϕ
X : Finset Formula
ϕ : Formula
notin : ϕ ∉ X
⊢ lengthOfSet (insert ϕ X) = lengthOfSet X + lengthOfFormula ϕ