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