Allow safety invariants and proofs to depend on lifetimes

Aeneas currently strips lifetimes, which means that lifetimes which are written in surface Rust syntax have no correlate in generated Lean code. This is problematic because it means that safety invariants or proofs which rely on named lifetimes cannot be translated to Hermes.

Consider the invariant on the `PtrInner` type:

https://github.com/google/zerocopy/blob/c6b794933a8d49481b9dded6ed99bc339202b41d/src/pointer/inner.rs#L30-L40

Imagine that we are not able to encode lifetimes in Hermes annotations (e.g., the `isValid` annotation on `PtrInner`). If we naively pretend that lifetimes don't exist, then consider `PtrInner::from_ref`:

https://github.com/google/zerocopy/blob/c6b794933a8d49481b9dded6ed99bc339202b41d/src/pointer/inner.rs#L129-L151

This safety proof relies on `'a`. If we ignored `'a`, we could get Hermes to accept the following code as sound:

```rust
pub(crate) fn from_ref<'b>(ptr: &'b T) -> PtrInner<'a, T> { ... }
```

This would allow us to do e.g.:

```rust
let x = 0usize;
let p = PtrInner::from_ref(&x);
drop(x);
// p is still alive, but points to freed memory
```

That's not just hypothetical. Today, we use `PtrInner` to build `Ptr`, e.g. via:

https://github.com/google/zerocopy/blob/c6b794933a8d49481b9dded6ed99bc339202b41d/src/pointer/ptr.rs#L173-L190

While the call to `Ptr::from_inner` has its own safety preconditions which must be proven, the `PtrInner` itself is responsible for handling the invariant that its referent allocation lives for `'a`. Thus, if we could convince Hermes to accept `fn from_ref<'b>(ptr: &'b T) -> PtrInner<'a, T>` as sound, then we could similarly convince Hermes to accept the following as sound:

```rust
pub fn from_ref<'b>(ptr: &'b T) -> Ptr<'a, T, ...> { ... }
```

Finally, we could combine this with `Ptr::as_ref`:

https://github.com/google/zerocopy/blob/c6b794933a8d49481b9dded6ed99bc339202b41d/src/pointer/ptr.rs#L232-L272

...to write the following 100% safe, obviously unsound code:

```rust
let x = 0usize;
let p = Ptr::from_ref(&x);
drop(x);
let r = p.as_ref();
println!("{}", *r); // Use after free!
```

In order to prevent code like this from being accepted by Hermes, Hermes needs to do one of the following:
- Detect and bail when a Hermes annotation mentions a lifetime
- Intentionally don't axiomatize any `unsafe` functions from the Rust standard library whose soundness depends on facts about lifetimes
- Figure out how to allow Hermes annotations to soundly mention lifetimes