Run crate coherence checks

[vakaras]

It seems that the compiler runs coherence checks (such as trait orphan check) in after_expansion implementation which, we do not do. We should fix this.

Creusot code that does this:

• https://github.com/xldenis/creusot/blob/3ddae2b7a3af964f223041eb581ff328a041fe84/creusot/src/callbacks.rs#L31-L37
• https://github.com/xldenis/creusot/blob/3ddae2b7a3af964f223041eb581ff328a041fe84/creusot/src/translation.rs#L33-L101