Function generalized_time_suffix 

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

{ if value.zone == TimeZone::Utc { seq![0x5au8] } else { Seq::empty() } }