Aeneas is flaky wrt nested mutable references

See https://github.com/google/zerocopy/pull/3223.

This shows up in the `test_2_6_nested_refs` test case:

```rust
/// ```lean, hermes
/// proof (h_progress):
/// sorry
/// proof context:
/// have h_foo : True := True.intro
/// ```
pub fn nested(x: &&u32, y: &mut &u32, z: &&mut u32) {
let _ = **x;
let _ = **y;
let _ = **z;
}
```

Sometimes this succeeds. Sometimes Aeneas panics with an "unimplemented" error.