Function u32_be_fmt 

pub open spec fn u32_be_fmt() -> U32BeFmt

{
    Mapped {
        inner: Fixed::<4>,
        mapper: (
            |i: Seq<u8>| u32_be_from_bytes(array_from_seq(i)),
            |o: u32| u32_be_to_bytes(o)@,
        ),
    }
}