Fix check_cast harness (model-checking#86)

Modifies the `check_cast` harness to:
- Be a proof instead of a proof for contract
- Remove the generic type parameter

Currently, Kani doesn't run this harness. (See the
[log](https://github.com/model-checking/verify-rust-std/actions/runs/10887990165/job/30211482361?pr=85)
from a recent PR). It doesn't run the harness because it has a generic
type parameter, and Kani's error handling for contract proofs doesn't
check for this condition. (PR to fix is
[here](model-checking/kani#3522)). Once we
remove the generic type parameter so that the harness runs, Kani
complains that we can't run it as a proof for contract because there are
no contracts, so we make it a regular proof instead.

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.

library/core/src/ptr/unique.rs

@@ -284,8 +284,8 @@ mod verify {
     }
 
     // pub const fn cast<U>(self) -> Unique<U>
-    #[kani::proof_for_contract(Unique::cast<U>)]
-    pub fn check_cast<U>() {
+    #[kani::proof]
+    pub fn check_cast() {
         let mut x : i32 = kani::any();
         let xptr = &mut x;
         unsafe {