pub open spec fn der_encodings_sorted(encodings: Seq<Seq<u8>>) -> bool
{ sorted_by(encodings, |a: Seq<u8>, b: Seq<u8>| der_octets_leq(a, b)) }