Function axiom_pack2_unpack 

pub broadcast proof fn axiom_pack2_unpack<T: ?Sized>(a: &mut T)

ensures

pack2(#[trigger] MutRef::unpack(a)) == a,