Function bool_fmt 

pub open spec fn bool_fmt<const DER: bool>() -> BoolFmt<DER>

{
    Mapped {
        inner: Refined(U8, |b: u8| DER ==> der_bool_byte(b)),
        mapper: (
            |b: u8| non_zero(b),
            |b: bool| if b { true_byte::<DER>() } else { FALSE_BYTE },
        ),
    }
}