Function ber_sequence_of_normalized_fmt 

pub open spec fn ber_sequence_of_normalized_fmt<C>(
    tag: Tag,
    content: C,
) -> ASN1Fmt<RepeatTillEnd<C>, BER>

{ ASN1Fmt(tag, RepeatTillEnd(content)) }

The definite-length BER encoding selected by BerSequenceOfFmt’s serializer.