rw [subsubClaim]
f : Formula
subsubClaim : projection {□f} = {f}
⊢ (projection {□f}).sum lengthOfFormula ≤ lengthOfFormula (□f)
f : Formula
subsubClaim : projection {□f} = {f}
⊢ {f}.sum lengthOfFormula ≤ lengthOfFormula (□f)