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