Function der_octets_drop_head 

pub open spec fn der_octets_drop_head(bytes: Seq<u8>) -> Seq<u8>

{ if bytes.len() == 0 { bytes } else { bytes.skip(1) } }