have subsubClaim : projection {□f} = {f} := by ext1; rw [proj]; simp
f : Formula
⊢ (projection {□f}).sum lengthOfFormula ≤ lengthOfFormula (□f)
f : Formula
subsubClaim : projection {□f} = {f}
⊢ (projection {□f}).sum lengthOfFormula ≤ lengthOfFormula (□f)