Function bits 

pub open spec fn bits<Repr: SpecByteLen, Tuple, Nominal>(
    repr: Repr,
    unpack: FnSpec<(Repr::T,), Tuple>,
    pack: FnSpec<(Tuple,), Repr::T>,
    refinement: PredFnSpec<Tuple>,
    ctor: FnSpec<(Tuple,), Nominal>,
    dtor: FnSpec<(Nominal,), Tuple>,
) -> Mapped<Refined<Mapped<Repr, BiMapper<Repr::T, Tuple>>, PredFnSpec<Tuple>>, BiMapper<Tuple, Nominal>>

{
    Mapped {
        inner: Refined(
            Mapped {
                inner: repr,
                mapper: BiMap(unpack, pack),
            },
            refinement,
        ),
        mapper: BiMap(ctor, dtor),
    }
}