Function generalized_time_prefix 

pub open spec fn generalized_time_prefix(value: GeneralizedTimeSpec) -> Seq<u8>

{
    decimal4_bytes(value.datetime.year)@ + decimal2_bytes(value.datetime.month)@
        + decimal2_bytes(value.datetime.day)@ + decimal2_bytes(value.datetime.hour)@
        + if value.precision == TimePrecision::Hour {
            Seq::empty()
        } else {
            decimal2_bytes(value.datetime.minute)@
                + if value.precision == TimePrecision::Second {
                    decimal2_bytes(value.datetime.second)@
                } else {
                    Seq::empty()
                }
        }
}