Function flatten_ber_bit_string_segments 

pub open spec fn flatten_ber_bit_string_segments(
    segments: Seq<BitStringSpec>,
) -> BitStringSpec

{
    let bits = segments.map(|_i: int, segment: BitStringSpec| segment.bits).flatten();
    BitStringSpec {
        unused: if bits.len() == 0 || segments.len() == 0 {
            0
        } else {
            segments.last().unused
        },
        bits,
    }
}