unfold projection
case bottom

⊢ (projection {bottom}).sum lengthOfFormula ≤ lengthOfFormula bottom
case bottom

⊢ (let X := {bottom};
        X.biUnion fun x => (formProjection x).toFinset).sum
      lengthOfFormula ≤
    lengthOfFormula bottom