Function true_byte 

pub open spec fn true_byte<const DER: bool>() -> u8

{ CANONICAL_TRUE_BYTE }