Unsafe implementations

An unsafe implementation is translated by implementing the associated proof.

// SAFETY: <justification>.
unsafe impl Send for Mutex {}

would translate to:

impl Send for Mutex {
    // SAFETY: <justification>.
    const P: Proof = Update(());
}