Function axiom_pin_has_resolved 

pub broadcast proof fn axiom_pin_has_resolved<'a, T: ?Sized>(pin: Pin<&'a mut T>)

ensures

has_resolved::<Pin<&'a mut T>>(pin)
    ==> (#[trigger] pin.mut_ref()).future.value() == pin.mut_ref().current,