Function lemma_der_encodings_sorted_index 

pub proof fn lemma_der_encodings_sorted_index(encodings: Seq<Seq<u8>>, i: int, j: int)

requires

der_encodings_sorted(encodings),

0 <= i < j < encodings.len(),

ensures

der_octets_leq(encodings[i], encodings[j]),