Function ber_sequence_of_fmt 

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

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

BER SEQUENCE OF accepting definite and indefinite outer length forms.

The indefinite branch is non-recursive at this layer: Repeat parses complete ASN.1 elements until EOC. Nested indefinite values are handled by the element codec itself. Serialization is normalized to the definite form.