feat(hax-lib): allow requires & ensures on &mut inputs functions

[W95Psp]

Fixes #755 and fixes #290.

This allows this kind of post-conditions:

#[hax::requires(*x < 40 && *y < 300)]
#[hax::ensures(|result| *future(x) == *y && *future(y) == *x && result == *x + *y)]
fn swap_and_mut_req_ens(x: &mut u32, y: &mut u32) -> u32 {
    let x0 = *x;
    *x = *y;
    *y = x0;
    *x + *y
}