Function asn1_fmt 

pub open spec fn asn1_fmt<Content: SpecCombinator, const DER: bool>(
    tag: Tag,
    content: Content,
) -> ASN1InnerFmt<Content, DER>

{
    Mapped {
        inner: PrefixTagged(
            TagFmt,
            tag,
            Bind(LengthFmt::<DER>, |len: usize| ExactLen(len, content)),
        ),
        mapper: (
            |i: (usize, Content::T)| i.1,
            |o: Content::T| (content.byte_len(o) as usize, o),
        ),
    }
}