ghost uses of never type invalidates borrowchecking

[tjhance]

Verus wrongly accepts this:

proof fn test(nvr: !) { }
proof fn consume<T>(tracked t: T) { }

proof fn test2<T>(tracked t: T) {
    test(arbitrary());

    consume(t);
    consume(t);
}

because the ghost use of the ! type causes Rust to think the consume statements are unreachable.