Function lemma_generalized_time_encode_roundtrip 

pub proof fn lemma_generalized_time_encode_roundtrip<const DER: bool>(
    value: GeneralizedTimeSpec,
)

requires

if DER { value.der_wf() } else { value.wf() },

generalized_time_len(value) <= usize::MAX,

ensures

generalized_time_wf::<DER>(generalized_time_bytes(value)),

generalized_time_value(generalized_time_bytes(value)) == Some(value),

generalized_time_bytes(value).len() == generalized_time_len(value),