Function generalized_time_to_bytes 

pub exec fn generalized_time_to_bytes<'a, Output: OutputBuf>(
    value: &GeneralizedTime<'a>,
    obuf: &mut Output,
)

requires

value.deep_view().wf(),

old(obuf).fits(generalized_time_bytes(value.deep_view()).len()),

ensures

final(obuf)@ == old(obuf)@ + generalized_time_bytes(value.deep_view()),

forall |n| {
    old(obuf).fits(generalized_time_bytes(value.deep_view()).len() + n)
        <==> final(obuf).fits(n)
},

old(obuf).same_destination(final(obuf)),

Writes a GeneralizedTime directly to an output buffer without allocating.