Post-condition on function in impl fails if function uses &mut Self

[karthikbhargavan]

#[hax_lib::attributes]
trait T {
    #[hax_lib::ensures(|_|true)]
    fn v(x:&mut Self);
}

Open this code snippet in the playground

error[E0411]: cannot find type `Self` in this scope
 --> src/lib.rs:4:17
  |
1 | #[hax_lib::attributes]
  | ---------------------- `Self` not allowed in a function
...
4 |     fn v(x:&mut Self);
  |                 ^^^^ `Self` is only available in impls, traits, and type definitions

Works if the ensures is removed.