[lifetime-generate] Trait bound is not satisfied (external impl of a trait)

[BLepers]

I am trying to specify the following code:

use vstd::prelude::*;

// Cannot be put in the verus!{} block because
// error: The verifier does not yet support the following Rust feature: &mut types, except in special cases
impl<T: 'static> ForeignOwnable for Box<T> {
    type Borrowed<'a> = &'a mut T;
}

verus!{
pub trait ForeignOwnable: Sized {
    type Borrowed<'a>;
}

struct A { a: i32 }
struct B {}

pub trait Operations: Sized {
    type QueueData: ForeignOwnable;
}

impl Operations for B {
    type QueueData = Box<A>;
}

fn main() {
    let a = Box::new(A { a: 1 });
}
}

Which gives the following error:

error: the trait bound `C<6, (std::boxed::Box<A>, std::boxed::Box<C<13, ()>>)>: T41_ForeignOwnable` is not satisfied
  --> test7.rs:20:1
   |
20 | impl Operations for B {
   | ^

error: aborting due to 1 previous error

Is there any way to make Verus realize that the ForeignOwnable trait is implemented for Box? I tried playing with external_trait_specification, but got nowhere...

[tjhance]

Looks like another lifetime-generate error