Improving the sequence library

Summarizing some discussions about the sequence library, gathering pain points and areas for improvement.

Aymeric:

• Need to call Seq.equal explicitly (JP: not sure there's much hope about this)
• Redundancy between BufferViews and the endianness lemmas in FStar.Kremlin.Endianness
• Had to re-do because stuff wasn't in ulib (move FStar.Kremlin.Endianness?)
• Vale uses nat64 (incompatible with UInt64.t)
• Manual calls: index/append, index/slice... doesn't seem to trigger well

Chris:

The axiom profiler points to our old friend, FStar.Seq.Properties.slice_slice. @nik and I have looked at slice_slice before and it looks completely innocent, but somehow it keeps showing up with enormous terms in a wide variety of situations. We believe it's not actually an infinite matching loop, but more of a large, yet, bounded matching explosion. Maybe it's time to figure out once and for all what's going on.

Tahina:

• Knew about the index_slice pattern with an unguarded forall in the post-condition.
• Claims that this: https://github.com/FStarLang/FStar/commit/a5df41ce315f0e38569c555c06327f3af577fd9f makes things behave better (but caused regressions, so not merged).

Jonathan:

• For the SHA algorithms, needed to add (with help from Tahina) these lemmas https://github.com/project-everest/hacl-star/blob/fstar-master/code/hash-new/Hacl.Hash.Lemmas.fst which make a lot of proofs go through more efficiently
• Note this bit: https://github.com/project-everest/hacl-star/blob/fstar-master/code/hash-new/Hacl.Hash.Core.SHA2.fst#L191 -- I had to call these lemmas myself and don't understand why index_slice didn't trigger properly