False positive: Outer function attributes are lost inside immediately invoked closures

[rikki322]

When using an immediately invoked closure (|| { ... })() inside a function with #[requires(...)] specifications, Prusti fails to propagate the outer function attributes into the closure's context.This leads to a false positive verification error.
Unlike other closure usages that trigger an [unsupported feature] error, this case attempts verification but fails due to missing context.
Reproduction

use prusti_contracts::*;

pub struct Vector {
    f: u32,
    g: u32,
}

#[pure]
#[requires(0 <= index && index < 2)]
pub fn is_equal(v: &Vector, index: usize, e: &u32) -> bool {
    if index == 0 {
        v.f == *e
    } else if index == 1 {
        v.g == *e
    } else {
        unreachable!()
    }
}

#[requires(0 <= index && index < 2)]
#[ensures(is_equal(v, index, result))]
#[trusted]
pub fn index(v: &Vector, index: usize) -> &u32 {
    (|| {
    if index == 0 {
        &v.f
    } else if index == 1 {
        &v.g
    } else {
        unreachable!()
    }
})()
}

fn main() {}

run prusti-rustc --edition=2018 main.rs
Expected Behavior
Prusti should report nothing or just report [unsupported feature]
Actual Behavior
Prusti reports:

error: [Prusti: verification error] unreachable!(..) statement might be reachable
  --> main.rs:30:9
   |
30 |         unreachable!()
   |         ^^^^^^^^^^^^^^
   |
   = note: this error originates in the macro `$crate::panic::unreachable_2015` which comes from the expansion of the macro `unreachable` (in Nightly builds, run with -Z macro-backtrace for more info)