unfold lengthOfSet
X : Finset Formula
ϕ : Formula
notin : ϕ ∉ X
⊢ lengthOfSet (insert ϕ X) = lengthOfSet X + lengthOfFormula ϕ
X : Finset Formula
ϕ : Formula
notin : ϕ ∉ X
⊢ (let X := insert ϕ X;
    X.sum lengthOfFormula) =
    (let X := X;
      X.sum lengthOfFormula) +
      lengthOfFormula ϕ