Aeneas is flaky wrt nested mutable references

[joshlf]

See #3223.

This shows up in the test_2_6_nested_refs test case:

/// ```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.