Function lemma_der_utc_time_canonical 

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

requires

utc_time_bytes_wf::<true>(bytes),

ensures

utc_time_bytes(utc_time_value(bytes)->0) == bytes,