Function lemma_der_generalized_time_canonical 

pub proof fn lemma_der_generalized_time_canonical(bytes: Seq<u8>)

requires

generalized_time_wf::<true>(bytes),

ensures

generalized_time_bytes(generalized_time_value(bytes).unwrap()) == bytes,