rw [Finset.sum_insert notin]
X : Finset Formula
ϕ : Formula
notin : ϕ ∉ X
⊢ (insert ϕ X).sum lengthOfFormula = X.sum lengthOfFormula + lengthOfFormula ϕ
X : Finset Formula
ϕ : Formula
notin : ϕ ∉ X
⊢ lengthOfFormula ϕ + ∑ x ∈ X, lengthOfFormula x = X.sum lengthOfFormula + lengthOfFormula ϕ