Engine: Mutable borrows on two-dimensional arrays not allowed

[karthikbhargavan]

Hax fails on the example below with the error [HAX0003] (DirectAndMut) The mutation of this &mut is not allowed here.
However, it could be accepted here since internal &mut annotations can be ignored in favor of the outer &mut for the purposes of hax.

fn f(z: &mut[&mut[u8]]) {
    z[0][0] = 32;
}

Open this code snippet in the playground