rw [Finset.sum_insert f_not_in_S]
f : Formula
S : Finset Formula
f_not_in_S : f ∉ S
IH : lengthOfSet (projection S) ≤ lengthOfSet S
⊢ (let X := projection (insert f S);
    X.sum lengthOfFormula) ≤
    let X := insert f S;
    X.sum lengthOfFormula
f : Formula
S : Finset Formula
f_not_in_S : f ∉ S
IH : lengthOfSet (projection S) ≤ lengthOfSet S
⊢ (let X := projection (insert f S);
    X.sum lengthOfFormula) ≤
    lengthOfFormula f + ∑ x ∈ S, lengthOfFormula x