Strictly speaking you put them in the header.

The first declaration of a function must include the contract pre/post conditions and follow-up re-declarations of the function must either not include any contract conditions or the same conditions as the initial declaration.

And you can avoid re-including the world because pre/post conditions should be externally visible behavior or call out to functions for pre/post checks on internal behavior.

Essentially you either define them using what you have in scope during the initial declaration or you call out to a function located elsewhere that can have access to more/internal scope and do more complicated checks.