Function ber_sequence_fmt 

pub open spec fn ber_sequence_fmt<C: SpecCombinator>(
    tag: Tag,
    content: C,
) -> Mapped<PrefixTagged<TagFmt, Tag, Bind<BerLengthFmt, FnSpec<(BerLength,), Sum<ExactLen<C, usize>, Pair<C, EocFmt>>>>>, FnSpecMapper<(BerLength, Sum<<C as SpecByteLen>::T, (<C as SpecByteLen>::T, (Tag, u8))>), <C as SpecByteLen>::T>>

{
    #[verusfmt::skip]
    Mapped {
        inner: PrefixTagged(
            TagFmt,
            tag,
            Bind(
                BerLengthFmt,
                |len: BerLength| match len {
                    BerLength::Definite(len) => L(ExactLen(len, content)),
                    BerLength::Indefinite => R(Pair(content, EOC)),
                },
            ),
        ),
        mapper: (
            |parsed: BerSequenceWireType<C::T>| match parsed.1 {
                L(value) => value,
                R((value, _eoc)) => value,
            },
            |value: C::T| {
                let len = content.byte_len(value) as usize;
                (BerLength::Definite(len), L(value))
            },
        ),
    }
}

BER SEQUENCE accepting definite and indefinite outer length forms.

content ends in super::BerEndFmt. ExactLen makes that marker observe the end of a bounded definite body; under indefinite framing it recognizes EOC without consuming it, after which Pair consumes EOC. Serialization is normalized to definite-length BER.