pub broadcast proof fn lemma_decode_pod_inverse<T: Pod>(v: T)Expand description
ensures
#[trigger] decode_pod::<T>(pod_bytes::<T>(v)) == v,Round-trip: decode_pod(pod_bytes(v)) == v by injectivity.