Function ber_bit_string_wire_wf 

pub open spec fn ber_bit_string_wire_wf(
    parsed: (Tag, Sum<(usize, BitStringSpec), Sum<(BerLength, Sum<Seq<BitStringSpec>, (Seq<BitStringSpec>, (Tag, u8))>), Never>>),
) -> bool

{
    match parsed.1 {
        L(_) => true,
        R(L((_length, inner))) => {
            match inner {
                L(segments) => ber_bit_string_segments_wf(segments),
                R((segments, _eoc)) => ber_bit_string_segments_wf(segments),
            }
        }
        R(R(_)) => true,
    }
}