Function lemma_asn1_start_identity_uint 

pub proof fn lemma_asn1_start_identity_uint(class: Class, number: u64)

ensures

asn1_start_identity(class, tag_num_from_uint(number))
    == asn1_start_identity_uint(class, number),

Numeric and TagNumber identity certificates denote the same two lead octets.