Function lemma_der_encodings_sorted_take 

pub proof fn lemma_der_encodings_sorted_take(encodings: Seq<Seq<u8>>, n: int)

requires

der_encodings_sorted(encodings),

0 <= n <= encodings.len(),

ensures

der_encodings_sorted(encodings.take(n)),