Well what you are trying to prove is that, given this constructor, there is no way to get an &mut ? in safe code to the same address you get an Pin<&mut ?> to, until after the destructor has run. But proving this is highly variegated based on the API exposed for that type.
2 Likes