Function utc_time_fmt 

pub open spec fn utc_time_fmt<const DER: bool>() -> Mapped<Refined<Tail, PredFnSpec<Seq<u8>>>, FnSpecMapper<Seq<u8>, UtcTime>>

{
    Mapped {
        inner: Refined(Tail, |bytes: Seq<u8>| utc_time_bytes_wf::<DER>(bytes)),
        mapper: (
            |bytes: Seq<u8>| utc_time_value(bytes)->0,
            |value: UtcTime| utc_time_bytes(value),
        ),
    }
}