Function ber_bit_string_rec_body 

pub open spec fn ber_bit_string_rec_body(
    tag: Tag,
    rec: ParamRecSpecs<Tag, BitStringSpec>,
) -> Mapped<Refined<Bind<TagFmt, FnSpec<(Tag,), Sum<Bind<LengthFmt<BER>, FnSpec<(usize,), ExactLen<BitStringFmt<BER>, usize>>>, Sum<Bind<BerLengthFmt, FnSpec<(BerLength,), Sum<ExactLen<RepeatTillEnd<BundledSpecs<BitStringSpec>>, usize>, Repeat<BundledSpecs<BitStringSpec>, EocFmt>>>>, Void>>>>, PredFnSpec<(Tag, Sum<(usize, BitStringSpec), Sum<(BerLength, Sum<Seq<BitStringSpec>, (Seq<BitStringSpec>, (Tag, u8))>), Never>>)>>, FnSpecMapper<(Tag, Sum<(usize, BitStringSpec), Sum<(BerLength, Sum<Seq<BitStringSpec>, (Seq<BitStringSpec>, (Tag, u8))>), Never>>), BitStringSpec>>

{
    #[verusfmt::skip]
    Mapped {
        inner: Refined(
            Bind(
                TagFmt,
                |parsed_tag: Tag| match parsed_tag {
                    t if t == primitive_tag(tag) => {
                        L(
                            Bind(
                                LengthFmt::<BER>,
                                |len: usize| ExactLen(len, BitStringFmt::<BER>),
                            ),
                        )
                    }
                    t if t == constructed_tag(tag) => {
                        R(
                            L(
                                Bind(
                                    BerLengthFmt,
                                    |len: BerLength| match len {
                                        BerLength::Definite(len) => {
                                            L(ExactLen(len, RepeatTillEnd(rec(TagFmt::BIT_STRING))))
                                        }
                                        BerLength::Indefinite => {
                                            R(Repeat(rec(TagFmt::BIT_STRING), EOC))
                                        }
                                    },
                                ),
                            ),
                        )
                    }
                    _ => {
                        R(
                            R(
                                Void(
                                    "Tag must match the configured BER BIT STRING identity",
                                ),
                            ),
                        )
                    }
                },
            ),
            |parsed: BerBitStringWireType| ber_bit_string_wire_wf(parsed),
        ),
        mapper: (
            |parsed: BerBitStringWireType| match parsed.1 {
                L((_len, value)) => value,
                R(L((_len, inner))) => {
                    match inner {
                        L(segments) => flatten_ber_bit_string_segments(segments),
                        R((segments, _eoc)) => flatten_ber_bit_string_segments(segments),
                    }
                }
                R(R(_)) => arbitrary(),
            },
            |value: BitStringSpec| (
                primitive_tag(tag),
                L((BitStringFmt::<BER>.byte_len(value) as usize, value)),
            ),
        ),
    }
}

One recursive unfolding of a BER BIT STRING.

IMPLICIT tagging replaces only the outer tag. Nested fragments retain universal BIT STRING tag 3, as required by X.690 §8.6.4.1.